Theorem 7.1.11 #26

New issue

Open

opened 2024-10-10 06:29:26 +00:00 by michael · 4 comments

michael commented

2024-10-10 06:29:26 +00:00

Owner

No description provided.

michael added this to the research project 2024-10-10 06:29:27 +00:00

michael changed title from ~~Theorem 7.1.1~~ to Theorem 7.1.11

2024-10-11 04:12:04 +00:00

michael referenced this issue

2024-10-11 04:12:12 +00:00

Chapter 7: Homotopy n-types #21

michael added the

stuck

label 2024-10-15 05:26:17 +00:00

michael commented

2024-10-15 05:28:02 +00:00

Author

Owner

Currently stuck on trying to prove that for some arbitrary (y : G) \rightarrow g \equiv y. This is just for the zero case 😱 The bounds are:

primGlue B T e
———— Boundary (wanted) —————————————————————————————————————
j = i0 ⊢ g
j = i1 ⊢ y
i = i0 ⊢ Acontr y j
i = i1 ⊢ Bcontr y j

TODO: Add a picture of my current ideas

Currently stuck on trying to prove that for some arbitrary $(y : G) \rightarrow g \equiv y$. This is just for the zero case 😱 The bounds are: ``` primGlue B T e ———— Boundary (wanted) ————————————————————————————————————— j = i0 ⊢ g j = i1 ⊢ y i = i0 ⊢ Acontr y j i = i1 ⊢ Bcontr y j ``` TODO: Add a picture of my current ideas

michael commented

2024-10-16 07:59:20 +00:00

Author

Owner

One attempt to do this was:

  eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
  eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y

  T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
  e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
  Uhh = primGlue ((y : B) → b ≡ y) T1 e1
      
  uhh : Uhh
  uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) {!  Bcontr !}

defining a separate glue type for the contr function itself. But this doesn't let me complete the hole...

One attempt to do this was: ``` eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y) eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) } e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) } Uhh = primGlue ((y : B) → b ≡ y) T1 e1 uhh : Uhh uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) {! Bcontr !} ``` defining a separate glue type for the contr function itself. But this doesn't let me complete the hole...

michael commented

2024-10-16 22:47:03 +00:00

Author

Owner

This won't work because I'm getting a path between the types (y:A) -> a==y and (y:B) -> b==y, but not between the particular values Acontr and Bcontr. Favonia's suggestion this morning is to use the fact that isContr itself is a prop

This won't work because I'm getting a path between the types `(y:A) -> a==y` and `(y:B) -> b==y`, but not between the particular values `Acontr` and `Bcontr`. Favonia's suggestion this morning is to use the fact that `isContr` itself is a prop

michael removed the

stuck

label 2024-10-20 19:06:02 +00:00

michael commented

2024-10-20 19:07:09 +00:00

Author

Owner

Ok, solved the first case in aa460fd5af, using Lemma 3.5.1 which says that if B : A \rightarrow \mathcal{U} is a prop for every (a : A), then if you have two pairs (p, q : \Sigma A B) then it's sufficient to just compare the first elements of them

However, I've only gotten it to work for a non PathP, because it expects the two types to agree. I tried for a little bit to write a PathP version of Lemma 3.5.1 but I haven't been successful yet

Ok, solved the first case in aa460fd5af21fb2da811e6e8af81cfacac2c1676, using Lemma 3.5.1 which says that if $B : A \rightarrow \mathcal{U}$ is a prop for every $(a : A)$, then if you have two pairs $(p, q : \Sigma A B)$ then it's sufficient to just compare the first elements of them However, I've only gotten it to work for a non `PathP`, because it expects the two types to agree. I tried for a little bit to write a `PathP` version of Lemma 3.5.1 but I haven't been successful yet