From 844a4ef9df7a90a3c5fddf773edbc98d8d166383 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 13 Dec 2023 22:35:24 +0300 Subject: [PATCH] Refactor equivalence-sym --- .../04-homotopies-and-equivalences.rzk.md | 94 ++++++++++++++----- 1 file changed, 68 insertions(+), 26 deletions(-) diff --git a/src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md b/src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md index e98a551..450c036 100644 --- a/src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk.md @@ -167,6 +167,23 @@ The traditional notion of isomorphism is poorly behaved for proof-relevant mathe and $(– \cdot p) : (z =_A x) \to (z =_A y)$ have quasi-inverses given by $(p^{−1} \cdot –)$ and $(– \cdot p^{−1})$, respectively. +#### Quasi-inverse has a quasi-inverse + +```rzk +#define inverse-from-qinv + ( A B : U) + ( f : A → B) + : qinv A B f → (B → A) + := \ (g , _) → g + +#define qinv-inverse-from-qinv + ( A B : U) + ( f : A → B) + : ( qinv-f : qinv A B f) + → qinv B A (inverse-from-qinv A B f qinv-f) + := \ (g , (α , β)) → (f , (β , α)) +``` + #### Quasi-inverse of the concatenation from the right side !!! tip "Change of variables in the code" @@ -248,7 +265,7 @@ One of numerous, but equivalent ways to define `isequiv`: !!! note "Definition 2.4.10." - $$\mathsf{isequiv}(f) :\equiv (\sum_{(g:B \to A)} (f \circ g \sim id_B)) \times (\sum_{(h:B \to A)} (h \circ f \sim id_A)).$$ + $$\mathsf{isequiv}(f) :\equiv \left(\sum_{(g:B \to A)} (f \circ g \sim id_B)\right) \times \left(\sum_{(h:B \to A)} (h \circ f \sim id_A)\right).$$ ```rzk #def isequiv @@ -261,7 +278,9 @@ One of numerous, but equivalent ways to define `isequiv`: ( Σ ( h : B → A) , homotopy A (\ _ → A) (compose A B A h f) (id A)) ``` -1. For the $\mathsf{qinv}(f) \to \mathsf{equiv}(f)$ direction, $g$ can play the role of both $g$ and $h$, i.e. we take $(g, \alpha, \beta)$ to $(g, \alpha, g, \beta)$. +### Proof of Property 1 + +For the $\mathsf{qinv}(f) \to \mathsf{isequiv}(f)$ direction, $g$ can play the role of both $g$ and $h$, i.e. we take $(g, \alpha, \beta)$ to $(g, \alpha, g, \beta)$. ```rzk #def qinv-to-isequiv @@ -271,7 +290,9 @@ One of numerous, but equivalent ways to define `isequiv`: := \ (g , (α , β)) → ((g , α) , (g , β)) ``` -2. For the other direction, we are given $(g, \alpha, h, \beta)$. Notice that $h \circ f \circ g \sim_{\alpha} h$ and $h \circ f \circ g \sim_{\beta} g$. Let $\gamma$ be the composite homotopy +### Proof of Property 2 + +For the other direction, we are given $(g, \alpha, h, \beta)$. Notice that $h \circ f \circ g \sim_{\alpha} h$ and $h \circ f \circ g \sim_{\beta} g$. Let $\gamma$ be the composite homotopy $$g \sim_{\beta^{-1}} h \circ f \circ g \sim_{\alpha} h,$$ @@ -307,60 +328,81 @@ One of numerous, but equivalent ways to define `isequiv`: ( β x))) -- h (f x) = id x ``` -3. Proof of the third property requires identifying the identity types of cartesian products and dependent pair types, which are discussed in Sections 2.6 and 2.7. +### Proof of Property 3 + +Proof of the third property requires identifying the identity types of cartesian products and dependent pair types, +which are discussed in Sections [2.6](06-cartesian-product-types.rzk.md) and [2.7](07-sigma-types.rzk.md). ## Equivalence of types + !!! lemma "Definition 2.4.11." - An equivalence from type $A$ to type $B$ is defined to be a function $f : A \to B$ together with an inhabitant of $\mathsf{equiv}(f)$. + An equivalence from type $A$ to type $B$ is defined to be a function $f : A \to B$ together with an inhabitant of $\mathsf{isequiv}(f)$. - $$(A \simeq B) :\equiv \Sigma_{(f:A \to B)} \mathsf{equiv}(f).$$ + $$(A \simeq B) :\equiv \sum_{(f:A \to B)} \mathsf{isequiv}(f).$$ !!! lemma "Note" - If we have a function $f : A \to B$ and we know that $e : \mathsf{equiv}(f)$, we may write $f : A \simeq B$, rather than $(f, e)$. + If we have a function $f : A \to B$ and we know that $e : \mathsf{isequiv}(f)$, we may write $f : A \simeq B$, rather than $(f, e)$. ```rzk #def equivalence - ( A B : U) + ( A B : U) : U := Σ (f : A → B) , isequiv A B f ``` ## Type equivalences are equivalence relations + !!! lemma "Lemma 2.4.12." + Type equivalence is an equivalence relation on $U$. More specifically: 1. For any $A$, the identity function $id_A$ is an equivalence; hence $A \simeq A$. 2. For any $f : A \simeq B$, we have an equivalence $f^{-1} : B \simeq A$. 3. For any $f : A \simeq B$ and $g : B \simeq C$, we have $g \circ f : A \simeq C$. -1. Reflexivity +### Reflexivity + ```rzk #def equivalence-refl - ( A : U) + ( A : U) : equivalence A A - := (id A , ((id A , \ x → refl) , (id A , \ x → refl))) + := + ( id A + , ( ( id A , \ x → refl) + , ( id A , \ x → refl))) ``` -2. Symmetry +### Symmetry + ```rzk +#def inverse-from-equivalence + ( A B : U) + : equivalence A B → (B → A) + := + \ (f , isequiv-f) → + inverse-from-qinv A B f (isequiv-to-qinv A B f isequiv-f) + +#def isequiv-inverse-from-equivalence + ( A B : U) + : ( f : equivalence A B) + → isequiv B A (inverse-from-equivalence A B f) + := + \ (f , isequiv-f) → + qinv-to-isequiv B A + ( inverse-from-equivalence A B (f , isequiv-f)) + ( qinv-inverse-from-qinv A B f (isequiv-to-qinv A B f isequiv-f)) + #def equivalence-sym - ( A B : U) + ( A B : U) : equivalence A B → equivalence B A - := \ (f , isequiv-f) → - ( first (isequiv-to-qinv A B f isequiv-f) - , qinv-to-isequiv - B - A - ( first (isequiv-to-qinv A B f isequiv-f)) - ( f - , ( second (second (isequiv-to-qinv A B f isequiv-f)) - , first (second (isequiv-to-qinv A B f isequiv-f)) - ) - ) - ) + := + \ f → + ( inverse-from-equivalence A B f + , isequiv-inverse-from-equivalence A B f) ``` -3. Transitivity +### Transitivity + ```rzk -- #def equivalence-trans -- (A B C : U)