Exercise 2.13: (2 ≃ 2) ≃ 2 #8

New issue

Closed

opened 2023-05-17 09:52:17 +00:00 by michael · 2 comments

michael commented

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

Owner

Show that (2 ≃ 2) ≃ 2.

Work

My proof strategy involves:

defining f : (2 ≃ 2) → 2 to be the forwards function, which maps any equivalence (e : 2 ≃ 2) to whatever (fst e) true is. this means if e is the same equivalence as id, then f e = true, but if e is the flipped equivalence, then f e = false
defining g : 2 → (2 ≃ 2) to be the backwards function, which maps true to id and false to neg
using a theorem Favonia suggested that I postulate (and then prove later), that two equivalences are identical if their functions are identical

The problem case occurs when I'm trying to prove g ∘ f ∼ id. I need to prove for any equivalence e, that (g ∘ f) e ≡ id e. However, since the equivalence function, (fst e), isn't known, I have to kind of reason about it in a roundabout way. These are the things I'm currently stuck on:

how can I prove that (fst e) true ≢ (fst e) false, given that I know (fst e) has an inverse? I am imagining some kind of strategy where I show that if they were the same, then the codomain of (fst e) is actually 1, resulting in 1 ≡ 2
The result I want is fst (g ((f e) true)) x ≡ (f e) x. I left it as a hole in the Agda code but I'm also not really sure how to use the previous result to show that the case where given that (fst e) true ≡ true, it's NOT true that (fst e) false ≡ true as well

Show that (2 ≃ 2) ≃ 2. [Work](https://git.mzhang.io/school/cubical/src/branch/master/src/HottBook/Chapter2Exercises.lagda.md#exercise-2-13) My proof strategy involves: - defining f : (2 ≃ 2) → 2 to be the forwards function, which maps any equivalence (e : 2 ≃ 2) to whatever (fst e) true is. this means if e is the same equivalence as id, then f e = true, but if e is the flipped equivalence, then f e = false - defining g : 2 → (2 ≃ 2) to be the backwards function, which maps true to id and false to neg - using a theorem Favonia suggested that I postulate (and then prove later), that two equivalences are identical if their functions are identical The problem case occurs when I'm trying to prove g ∘ f ∼ id. I need to prove for any equivalence e, that (g ∘ f) e ≡ id e. However, since the equivalence function, (fst e), isn't known, I have to kind of reason about it in a roundabout way. These are the things I'm currently stuck on: - how can I prove that (fst e) true ≢ (fst e) false, given that I know (fst e) has an inverse? I am imagining some kind of strategy where I show that if they were the same, then the codomain of (fst e) is actually 1, resulting in 1 ≡ 2 - The result I want is fst (g ((f e) true)) x ≡ (f e) x. I left it as a hole in the Agda code but I'm also not really sure how to use the previous result to show that the case where given that (fst e) true ≡ true, it's NOT true that (fst e) false ≡ true as well

michael added this to the (deleted) project 2023-05-17 09:52:18 +00:00

michael added the

exercise

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

michael referenced this issue

2023-05-17 09:53:35 +00:00

Chapter 2: Homotopy type theory #7

michael added a new dependency 2023-05-17 09:53:39 +00:00

#7 Chapter 2: Homotopy type theory

michael added the

T-equivalence

label 2023-05-17 09:55:36 +00:00

michael commented

2024-04-22 01:35:50 +00:00

Author

Owner

Having difficulty with the case of:

given that aux1 is a function that maps id -> true and neg -> false by just running the function on true
given that rev is a function that maps true -> id and false -> neg and giving the equivalence
prove that \texttt{aux1} \circ \texttt{rev} \sim \texttt{id}
- do this by proving that for every possible equivalence e between bools, (\texttt{aux1} \circ \texttt{rev}) ~ e \equiv \texttt{id} ~ e
- this is the same as (\texttt{rev} ((e \cdot l) \texttt{true}) \equiv e). to simplify let f = e \cdot l (the first projection of e )
- the problem is f is unknown to us, other than the fact that it has an inverse (given by e \cdot r )
  - need to prove that as long as f : \mathbb{2} \rightarrow \mathbb{2} has an inverse, then f(\texttt{true}) and f(\texttt{false}) must have different values. i'm not sure how to state this formally yet

Having difficulty with the case of: - given that `aux1` is a function that maps id -> true and neg -> false by just running the function on true - given that `rev` is a function that maps true -> id and false -> neg and giving the equivalence - prove that $\texttt{aux1} \circ \texttt{rev} \sim \texttt{id}$ - do this by proving that for every possible equivalence $e$ between bools, $(\texttt{aux1} \circ \texttt{rev}) ~ e \equiv \texttt{id} ~ e$ - this is the same as $(\texttt{rev} ((e \cdot l) \texttt{true}) \equiv e)$. to simplify let $f = e \cdot l$ (the first projection of $e$ ) - the problem is $f$ is unknown to us, other than the fact that it has an inverse (given by $e \cdot r$ ) - [ ] need to prove that as long as $f : \mathbb{2} \rightarrow \mathbb{2}$ has an inverse, then $f(\texttt{true})$ and $f(\texttt{false})$ _must_ have different values. i'm not sure how to state this formally yet

michael commented

2024-04-25 19:27:16 +00:00

Author

Owner

Notes from 2024-04-26 meeting with Favonia

Equivalences are the same if their functions are the same. Prove this
- Need to relate the g-id and h-id between two equivalences
- Could postulate it to finish this and then prove it later

Notes from 2024-04-26 meeting with Favonia - Equivalences are the same if their functions are the same. Prove this - Need to relate the g-id and h-id between two equivalences - Could postulate it to finish this and then prove it later

michael closed this issue

2024-05-08 23:34:24 +00:00