From 9fcef57a146eb33ecde9af61594999d203f1c079 Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Sun, 1 Oct 2023 18:45:55 +0200 Subject: [PATCH] Add 2.4.{4,7,8} --- .../01-types-are-higher-groupoids.rzk.md | 31 +++ .../04-homotopies-are-equivalences.rzk.md | 203 +++++++++++++++++- 2 files changed, 232 insertions(+), 2 deletions(-) diff --git a/src/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk.md b/src/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk.md index 6bf10cf..9c9df10 100644 --- a/src/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk.md @@ -142,4 +142,35 @@ Alternativerly, groupoids can be viewed as a generalization of groups, where not -- path-concat A x' z' w' q' r' = path-concat A x' z' w' q' r' ) (\ x' z' q' w' r' → refl) x y p) z q w r +``` + +## Related statements used in further proofs: + +!!! note "Concatencation of three paths" + +```rzk +#def 3-path-concat + (A : U) + (x y z w : A) + : (x = y) → (y = z) → (z = w) → (x = w) + := \ p q r → path-concat A x z w (path-concat A x y z p q) r +``` + +!!! note "Associativity symmetrical to 2.1.4-4" + $$(p \cdot q) \cdot r = p \cdot (q \cdot r)$$ + +```rzk +#def concat-assoc-2 + (A : U) + (x y z w : A) + (p : x = y) + (q : y = z) + (r : z = w) + : path-concat A x z w (path-concat A x y z p q) r = + path-concat A x y w p (path-concat A y z w q r) + := path-sym + (x = w) + (path-concat A x y w p (path-concat A y z w q r)) + (path-concat A x z w (path-concat A x y z p q) r) + (concat-assoc A x y z w p q r) ``` \ No newline at end of file diff --git a/src/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk.md b/src/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk.md index fa25950..0158aa1 100644 --- a/src/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk.md @@ -111,6 +111,7 @@ This is a literate Rzk file: Here $f(x)$ denotes the ordinary application of $f$ to $x$, while $f(H(x))$ denotes $ap_f(H(x))$. +Proof is given in the end of the file. ```rzk -- #def homotopy-id-swap -- (A : U) @@ -133,10 +134,135 @@ The traditional notion of isomorphism is poorly behaved for proof-relevant mathe : U := Σ (g : B → A), prod - (homotopy B (\ _ → B) (compose B A B f g) (id B)) - (homotopy A (\ _ → A) (compose A B A g f) (id A)) + (homotopy B (\ _ → B) (compose B A B f g) (id B)) + (homotopy A (\ _ → A) (compose A B A g f) (id A)) ``` +### Examples +!!! note "Example 2.4.7. Identity quasi-inverse" + The identity function $id_A : A \to A$ has a quasi-inverse given by $id_A$ itself, together with homotopies defined by $\alpha(y) :\equiv \mathsf{refl}_y$ and $\beta(x) :\equiv \mathsf{refl}_x$. + +```rzk +#def qinv-id + (A : U) + : qinv A A (id A) + := (id A, + (\ x → refl, + \ x → refl)) +``` + +!!! note "Example 2.4.8. Quasi-inverse for path concatenation" + For any $p : x =_A y$ and $z : A$, the functions $(p \cdot –) : (y =_A z) \to (x =_A z)$ 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 of the concatenation from the right side.** + +!!! note "Change of variables in the code" + Note the change of variables: $p \mapsto q, x \mapsto y, y \mapsto z, z \mapsto x$. That is, the code corrsesponds to the statement that for any $q : y =_A z$ and $x : A$, the function $(– \cdot q) : (x =_A y) \to (x =_A z)$ have quasi-inverse given by $(– \cdot q^{−1})$, respectively. + + +```rzk title="Definition of right concatenation as a function, and its inverse" +#def right-concat + (A : U) + (x y z : A) + (q : y = z) + : (x = y) → (x = z) + := \ p → path-concat A x y z p q + + +#def right-concat-inv + (A : U) + (x y z : A) + (q : y = z) + : (x = z) → (x = y) + := right-concat A x z y (path-sym A y z q) + +``` + +```rzk title="Proofs that both compositions are homotopical to identity" +#def right-concat-right-inv-remove-refl + (A : U) + (x y z : A) + (p : x = y) + (q : y = z) + : (compose (x = y) (x = z) (x = y) (right-concat-inv A x y z q) (right-concat A x y z q)) p = p + := 3-path-concat + (x = y) -- type of things that are connected my paths + -- 1st point: (p • q) • q⁻¹ + (compose (x = y) (x = z) (x = y) (right-concat-inv A x y z q) (right-concat A x y z q) p) + -- 2nd point: p • (q • q⁻¹) + (path-concat A x y y p (path-concat A y z y q (path-sym A y z q))) + -- 3rd point: p • refl + (path-concat A x y y p refl) + -- 4th point: p + p + -- 1st proof: (p • q) • q⁻¹ = p • (q • q⁻¹) + (concat-assoc-2 A x y z y + p + q + (path-sym A y z q) + ) + -- 2nd proof: p • (q • q⁻¹) = p • refl + (ap + (y = y) + (x = y) + (\ p' → (path-concat A x y y p p')) + (path-concat A y z y q (path-sym A y z q)) + refl + (inverse-r A y z q) + ) + -- 3rd proof: p • refl = p + (path-sym (x = y) p (path-concat A x y y p refl) (concat-refl A x y p)) + + +#def right-concat-left-inv-remove-refl + (A : U) + (x y z : A) + (r : x = z) + (q : y = z) + : (compose (x = z) (x = y) (x = z) (right-concat A x y z q) (right-concat-inv A x y z q)) r = r + := 3-path-concat + (x = z) -- type of things that are connected my paths + -- 1st point: (r • q⁻¹) • q + (compose (x = z) (x = y) (x = z) (right-concat A x y z q) (right-concat-inv A x y z q) r) + -- 2nd point: r • (q⁻¹ • q) + (path-concat A x z z r (path-concat A z y z (path-sym A y z q) q)) + -- 3rd point: r • refl + (path-concat A x z z r refl) + -- 4th point: p + r + -- 1st proof: (r • q⁻¹) • q = r • (q⁻¹ • q) + (concat-assoc-2 A x z y z + r + (path-sym A y z q) + q + ) + -- 2nd proof: r • (q⁻¹ • q) = r • refl + (ap + (z = z) + (x = z) + (\ p' → (path-concat A x z z r p')) + (path-concat A z y z (path-sym A y z q) q) + refl + (inverse-l A y z q) + ) + -- 3rd proof: r • refl = r + (path-sym (x = z) r (path-concat A x z z r refl) (concat-refl A x z r)) +``` + +```rzk title="Proof for quasi-inverse of right concatenation" +#def right-concat-inv-is-qinv-for-right-concat + (A : U) + (x y z : A) + (q : y = z) + : qinv (x = y) (x = z) (right-concat A x y z q) + := (right-concat-inv A x y z q, + ( + \ (r : x = z) → right-concat-left-inv-remove-refl A x y z r q, + \ (p : x = y) → right-concat-right-inv-remove-refl A x y z p q + )) +``` + + ## Equivalences An improved notion, `isequiv`, has the following properties: @@ -271,4 +397,77 @@ meaning $\gamma(x) :\equiv \beta(g(x))^{-1} \cdot h(\alpha(x))$. Now define $\be -- (A B C : U) -- : equivalence A B → equivalence B C → equivalence A C -- := \ (f, isequiv-f) (g, isequiv-g) → +``` + + + +``` title="Proof for corollary 2.4.4. Homotopy with id" +lemma 2.4.3 : H(x) • g (p) = f (p) • H y + +Substitutions: +x → f x +y → x +g → id +p → H x + +Result of application of lemma with the corresponding values: +H(f x) • id (H x) = f (H x) • H x + + +By right-concatenating (H x)⁻¹ to the both sides, we have +H(f x) = H(f x) • id (H x) • (H x)⁻¹ = f (H x) • H x • (H x)⁻¹ = f (H x) +``` + + +```rzk +#def homotopy-id-swap + (A : U) + (f : A → A) + (H : homotopy A (\ _ → A) f (id A)) + (x : A) + : H (f x) = ap A A f (f x) (id A x) (H x) + := 3-path-concat + (f (f x) = (f x)) -- type of points + -- 1st point: H (f x) + (H (f x)) + -- 2nd point: (H (f x) • (H x)) • (H x)⁻¹ + (path-concat A (f (f x)) x (f x) (path-concat A (f (f x)) (f x) x (H (f x)) (H x)) (path-sym A (f x) x (H x))) + -- 3rd point: (f (H x) • (H x)) • (H x)⁻¹ + (path-concat A (f (f x)) x (f x) (path-concat A (f (f x)) (f x) x (ap A A f (f x) x (H x)) (H x)) (path-sym A (f x) x (H x))) + -- 4th point: f (H x) + (ap A A f (f x) x (H x)) + -- proof that H (f x) = (H (f x) • H x) • (H x)⁻¹ + (path-sym + (f (f x) = f x) + (path-concat A (f (f x)) x (f x) (path-concat A (f (f x)) (f x) x (H (f x)) (H x)) (path-sym A (f x) x (H x))) + (H (f x)) + (right-concat-right-inv-remove-refl A (f (f x)) (f x) x (H (f x)) (H x))) + -- proof that (H (f x) • H x) • (H x)⁻¹ = (f (H x) • (H x)) • (H x)⁻¹ + (ap + (f (f x) = x) -- (type of domain) + (f (f x) = f x) -- (type of codomain) + (\ p' → path-concat A (f (f x)) x (f x) p' (path-sym A (f x) x (H x))) + -- function-to-apply: whiskering by (Hx)⁻¹, a.k.a. cancel out H x + (path-concat A (f (f x)) (f x) x (H (f x)) (H x)) -- left point in path below + (path-concat A (f (f x)) (f x) x (ap A A f (f x) x (H x)) (H x)) -- right point in path below + (path-concat + (f (f x) = x) + -- (H (f x) • H x) + (path-concat A (f (f x)) ((\ (z : A) → z) (f x)) ((\ (z : A) → z) x) (H (f x)) (H x)) + -- (H (f x) • id (H x)) + (path-concat A (f (f x)) ((\ (z : A) → z) (f x)) ((\ (z : A) → z) x) (H (f x)) (ap A A (\ (z : A) → z) (f x) x (H x))) + -- f (H x) • (H x) + (path-concat A (f (f x)) (f x) ((\ (z : A) → z) x) (ap A A f (f x) x (H x)) (H x)) + -- (H (f x) • H x) = (H (f x) • id (H x)) + (ap + (f x = x) -- domain + ((f (f x)) = x) -- codomain + (\p' → path-concat A (f (f x)) ((\ (z : A) → z) (f x)) ((\ (z : A) → z) x) (H (f x)) p') -- action of concatenation + ( H x ) -- left point in path + (ap A A (\ z → z) (f x) x (H x)) -- right point in path + (path-sym (f x = x) (ap A A (\ z → z) (f x) x (H x)) (H x) (ap-id A (f x) x (H x)))) + -- (H (f x) • id (H x)) = f (H x) • (H x) + (hom-naturality A A f (\ z → z) H (f x) x (H x)))) + -- proof that (f (H x) • (H x)) • (H x)⁻¹ = f (H x) + (right-concat-right-inv-remove-refl A (f (f x)) (f x) x (ap A A f (f x) (id A x) (H x)) (H x)) ``` \ No newline at end of file