Exercise 2.4: n-dimensional path #6

New issue

Closed

opened 2023-05-15 23:27:47 +00:00 by michael · 2 comments

michael commented

2023-05-15 23:27:47 +00:00

Owner

Exercise 2.4: Define, by induction on n, a general notion of n-dimensional
path in a type A, simultaneously with the type of boundaries of such paths

Work

Exercise 2.4: Define, by induction on n, a general notion of n-dimensional path in a type A, simultaneously with the type of boundaries of such paths [Work](https://git.mzhang.io/school/cubical/src/branch/master/src/HottBook/Chapter2Exercises.lagda.md#exercise-2-4)

michael referenced this issue

2023-05-16 14:05:07 +00:00

Chapter 2: Homotopy type theory #7

michael added a new dependency 2023-05-16 14:05:24 +00:00

#7 Chapter 2: Homotopy type theory

michael added this to the (deleted) project 2023-05-16 14:05:39 +00:00

michael commented

2023-05-16 16:59:47 +00:00

Author

Owner

Just putting some old attempts here:

-- data nPath {A : Type} : ℕ → Type where                          
--   zeroPath : (x y : A) → (p : x ≡ y) → nPath zero               
--   sucPath : {n : ℕ}                                             
--     → (left : nPath n)                                          
--     → (right : nPath n)                                         
--     → (p : left ≡ right)                                        
--     → nPath (suc n)                                             
                                                                   
-- data nPath : (A : Type) → (x y : A) → Type where                
--   path-zero : (A : Type) → (x y : A) → (p : x ≡ y) → nPath A x y
--   path-suc : (A : Type) → (x y : A)                             
--     → (left : nPath A x y)                                      
--     → (right : nPath A x y)                                     
--     → (p : left ≡ right)                                        
--     → nPath (nPath A x y) left right

For this to work, all of these must be tracked in the type:

p : (2 ≡ 1 + 1)
p = refl       
               
q : (2 ≡ 1 + 1)
q = ?          
               
p2 : p ≡ q     
q2 : p ≡ q     
               
p3 : p2 ≡ q2

Just putting some old attempts here: ```agda -- data nPath {A : Type} : ℕ → Type where -- zeroPath : (x y : A) → (p : x ≡ y) → nPath zero -- sucPath : {n : ℕ} -- → (left : nPath n) -- → (right : nPath n) -- → (p : left ≡ right) -- → nPath (suc n) -- data nPath : (A : Type) → (x y : A) → Type where -- path-zero : (A : Type) → (x y : A) → (p : x ≡ y) → nPath A x y -- path-suc : (A : Type) → (x y : A) -- → (left : nPath A x y) -- → (right : nPath A x y) -- → (p : left ≡ right) -- → nPath (nPath A x y) left right ``` For this to work, all of these must be tracked in the type: ```agda p : (2 ≡ 1 + 1) p = refl q : (2 ≡ 1 + 1) q = ? p2 : p ≡ q q2 : p ≡ q p3 : p2 ≡ q2 ```

michael added the

exercise

label 2023-05-17 09:52:42 +00:00

michael changed title from ~~N dimensional path (2.4)~~ to Exercise 2.4: n-dimensional path

2023-05-17 09:52:56 +00:00

michael modified the project from (deleted) to research

2024-05-24 01:34:36 +00:00

michael commented

2024-07-25 02:15:31 +00:00

Author

Owner

Ended up going with:

data n-path {l : Level} : {A : Set l} → (x y : A) → Set (lsuc l) where
  zero : {A : Set l} → {x y : A} → x ≡ y → n-path x y
  suc : {A : Set l} → {x y : A} → {p q : x ≡ y} → p ≡ q → n-path p q

Ended up going with: ```agda data n-path {l : Level} : {A : Set l} → (x y : A) → Set (lsuc l) where zero : {A : Set l} → {x y : A} → x ≡ y → n-path x y suc : {A : Set l} → {x y : A} → {p q : x ≡ y} → p ≡ q → n-path p q ```

michael closed this issue

2024-07-25 02:15:31 +00:00