From d0b5465526cfcbcfbb146a9f290cadcf619f0c6e Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Wed, 11 Oct 2023 18:44:13 -0700 Subject: [PATCH 01/25] begin work on some homotopy coherences --- src/hott/01-paths.rzk.md | 13 ++++++++++ src/hott/02-homotopies.rzk.md | 48 +++++++++++++++++++++++++++++++++++ 2 files changed, 61 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index ac43faf0..fa636f5a 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -380,6 +380,19 @@ The following needs to be outside the previous section because of the usage of ( concat-concat' A x y z q r))) ``` +A special case of this is sometimes useful + +```rzk +#def cancel-left-path + (A : U) + (x y : A) + (p q : x = y) + : (p = q) → ( concat A y x y (rev A x y q) p) = refl + := \ α → + triangle-rotation A x y y p q refl α + +``` + ### Concatenation with a path and its reversal ```rzk diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index 70132dd9..c44c7237 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -41,10 +41,58 @@ This is a literate `rzk` file: Homotopy composition is defined in diagrammatic order like `#!rzk concat` but unlike composition. +The following is the unit for compositions of homotopies. + +```rzk +#def refl-htpy + (f : A → B) + : homotopy f f + := \ x → refl +``` + ```rzk #end homotopies ``` +There is also a dependent version of homotopy. + +```rzk +#def dependent-homotopy + ( A : U) + ( B : A → U) + (f g : (a : A) → B a) + : U + := (a : A) → (f a = g a) +``` + +## Some path algebra for homotopies + +This section contains some lemmas on the groupoidal structure of homotopies. + +Given a homotopy between two homotopies $C : H \sim K$ this produces a homotopy +$K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ + +```rzk +#def htpy-cancel-left + (A B : U) + (f g : A → B) + (H K : homotopy A B f g) + (C : dependent-homotopy A (\ a → f a = g a) H K) + : dependent-homotopy + A + (\ b → g b = g b) + (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) + (refl-htpy A B g) + := \ x → + cancel-left-path + (B) + (f x) + (g x) + (H x) + (K x) + (C x) +``` + ## Whiskering homotopies ```rzk From 4770abac31f230e091f61f6605445aa36eecbf4a Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Wed, 11 Oct 2023 20:36:27 -0700 Subject: [PATCH 02/25] added the eq-top-cancel function --- src/hott/01-paths.rzk.md | 64 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index fa636f5a..b1c4ce42 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -965,3 +965,67 @@ The following is the same as above but with alternating arguments. ( r) ( H) ``` + +The function below represents a somewhat special situation, which nevertheless +arises when dealing with certain naturality diagrams. One has a commutative +square and a path that cancels that top path. Then the type below witnesses the +equivalence between the right side of the square and a particular zig-zag of +paths. + +```rzk +#def eq-top-cancel-commutative-square + (A : U) + (v w y z : A) + (p : v = w) + (q : w = v) + (s : w = y) + (r : v = z) + (t : y = z) + (H : (concat A w v z q r) = (concat A w y z s t)) + (H' : (concat A v w v p q) = refl) + : r = (concat A v w z p (concat A w y z s t)) + := + (concat + (v = z) + ( r ) + ( concat A v v z refl r) + ( concat A v w z p (concat A w y z s t) ) + (rev + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + (concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev + ( v = z ) + (concat A v v z (concat A v w v p q) r ) + (concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) +``` From 0710acfd897b1638465ed4a7c03ac0992ddbfd47 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Thu, 12 Oct 2023 15:56:53 -0700 Subject: [PATCH 03/25] added an svg commutative diagram --- src/hott/01-paths.rzk.md | 88 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 86 insertions(+), 2 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index b1c4ce42..1fd50a91 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -969,8 +969,92 @@ The following is the same as above but with alternating arguments. The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the -equivalence between the right side of the square and a particular zig-zag of -paths. +equivalence between the right side of the square (in blue) and a particular +zig-zag of paths, the red zig-zag. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def eq-top-cancel-commutative-square From 8a1bef15e06d529eb12a16300cb7ed605eb156d8 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Fri, 13 Oct 2023 16:29:00 -0700 Subject: [PATCH 04/25] added a utility for path coherence --- src/hott/01-paths.rzk.md | 204 +++++++++++++++++++++------------------ 1 file changed, 112 insertions(+), 92 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index 1fd50a91..e023b629 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -975,86 +975,86 @@ zig-zag of paths, the red zig-zag. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def eq-top-cancel-commutative-square @@ -1080,11 +1080,11 @@ zig-zag of paths, the red zig-zag. ( r ) (left-unit-concat A v z r)) (concat - ( v = z) - ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v w z p (concat A w y z s t )) - (rev + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev ( v = z ) (concat A v v z (concat A v w v p q) r ) (concat A v v z refl r) @@ -1097,13 +1097,13 @@ zig-zag of paths, the red zig-zag. ( refl ) ( H') ( r) )) - ( concat - ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) - ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right ( A ) ( v ) ( w) @@ -1113,3 +1113,23 @@ zig-zag of paths, the red zig-zag. ( concat A w y z s t) ( H))))) ``` + +```rzk + +#def htpy-id-cancel-left-concat-left-eq + (A : U) + (a b : A) + (p : a = b) + (q : a = b) + (H : p = q) + (r : b = a) + (H' : (concat A a b a q r) = refl) + : (concat A a b a p r) = refl + := concat + ( a = a) + ( concat A a b a p r ) -- begin + ( concat A a b a q r ) -- middle + ( refl ) -- end + ( concat-eq-left A a b a p q H r) + ( H' ) +``` From 7e6c2642176aff170656d485256514b5c996a872 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Fri, 13 Oct 2023 16:35:08 -0700 Subject: [PATCH 05/25] added commutative diagram for new utility --- src/hott/01-paths.rzk.md | 66 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index e023b629..d1bfb2ba 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -1114,6 +1114,72 @@ zig-zag of paths, the red zig-zag. ( H))))) ``` + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def htpy-id-cancel-left-concat-left-eq From f065390f137ee8d93b88d4189b3ae31696509506 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sat, 14 Oct 2023 20:49:13 -0700 Subject: [PATCH 06/25] some complicated coherences added --- src/hott/01-paths.rzk.md | 142 ++++++++++++---- src/hott/02-homotopies.rzk.md | 36 ++-- src/hott/04-half-adjoint-equivalences.rzk.md | 167 +++++++++++++++++++ 3 files changed, 296 insertions(+), 49 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index d1bfb2ba..a5e5e6f8 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -970,7 +970,8 @@ The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the equivalence between the right side of the square (in blue) and a particular -zig-zag of paths, the red zig-zag. +zig-zag of paths, the red zig-zag. We choose the assocativity order for the +triple compostion for ease of use in a later proof. @@ -1070,48 +1071,112 @@ zig-zag of paths, the red zig-zag. : r = (concat A v w z p (concat A w y z s t)) := (concat - (v = z) - ( r ) - ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t) ) - (rev (v = z) - (concat A v v z refl r ) ( r ) - (left-unit-concat A v z r)) - (concat - ( v = z) ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v w z p (concat A w y z s t )) + ( concat A v w z p (concat A w y z s t) ) (rev - ( v = z ) - (concat A v v z (concat A v w v p q) r ) - (concat A v v z refl r) - ( concat-eq-left - ( A) - ( v) - ( v) - ( z) - ( concat A v w v p q ) - ( refl ) - ( H') - ( r) )) - ( concat + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + (concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev + ( v = z ) + (concat A v v z (concat A v w v p q) r ) + (concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) +``` + +```rzk +#def eq-top-cancel-commutative-square' + (A : U) + (v w y z : A) + (p : v = w) + (q : w = v) + (s : w = y) + (r : v = z) + (t : y = z) + (H : (concat A w v z q r) = (concat A w y z s t)) + (H' : (concat A v w v p q) = refl) + : r = ( concat A v y z (concat A v w y p s) t) + := + (concat ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) + ( r) ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right - ( A ) - ( v ) - ( w) - ( z) - ( p) - ( concat A w v z q r) - ( concat A w y z s t) - ( H))))) + ( concat A v y z (concat A v w y p s) t) + ( concat + ( v = z) + ( r ) + ( concat A v v z refl r) + ( concat A v w z p (concat A w y z s t) ) + ( rev + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + ( concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + ( rev + ( v = z ) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) + ( rev-associative-concat A v w y z p s t)) ``` @@ -1180,6 +1245,9 @@ zig-zag of paths, the red zig-zag. +If $H \sim K$ is a homotopy between homotopies, then we can cancel on the left +to get $$ K^{-1} \cdot H \sim \texttt{refl}$$ + ```rzk #def htpy-id-cancel-left-concat-left-eq diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index c44c7237..aeb2840c 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -74,23 +74,17 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ```rzk #def htpy-cancel-left - (A B : U) - (f g : A → B) - (H K : homotopy A B f g) - (C : dependent-homotopy A (\ a → f a = g a) H K) - : dependent-homotopy + (A B : U) + (f g : A → B) + (H K : homotopy A B f g) + (C : dependent-homotopy A (\ a → f a = g a) H K) + : dependent-homotopy A (\ b → g b = g b) (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) (refl-htpy A B g) := \ x → - cancel-left-path - (B) - (f x) - (g x) - (H x) - (K x) - (C x) + cancel-left-path (B) (f x) (g x) (H x) (K x) (C x) ``` ## Whiskering homotopies @@ -161,6 +155,24 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ( p) ``` +It is sometimes useful to have this reverse + +```rzk +#def rev-nat-htpy + ( A B : U) + ( f g : A → B) + ( H : homotopy A B f g) + ( x y : A) + ( p : x = y) + : ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) = + ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) + := rev + ( f x = g y) + ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) + ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) + ( nat-htpy A B f g H x y p) +``` + ```rzk title="Naturality in another form" #def triple-concat-nat-htpy ( A B : U) diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index b26e911f..e8489163 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -804,3 +804,170 @@ have equivalent identity types by showing that equivalences are embeddings. : Equiv (x = y) (f x = f y) := (ap A B x y f , is-emb-is-equiv A B f is-equiv-f x y) ``` + +## Some further useful coherences + +For a half-adjoint equivalence $f$ with inverse $g$ and coherence +$G ⋅ f ∼ \text{ap}_f ⋅ H$ we show + +$$ +\text{ap}_f (H^{-1} a) ⋅ G (f a) = \texttt{refl}_{f (a)}. +$$ + +This is a consequence of cancelling the coherence on the left, and then applying +the equality $\text{ap}_f (H^{-1} a) = (\text{ap}_f (H a))^{-1}$. It is +cumbersome to state and prove only becaues of data revtrieval and the number of +reversals. + +```rzk +#def ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae + (A B : U) + (f : A → B) + (a : A) + (b : B) + (q : (f a) = b) + (is-hae : is-half-adjoint-equiv A B f) + : (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a ))) + ( f a) + (ap ( A) ( B) + ( a) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) ( f a))) + ( f) + ( rev ( A) + ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ((retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a))) + = refl + := + htpy-id-cancel-left-concat-left-eq + ( B) + (f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( ap ( A) ( B) + ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) ( f a))) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( rev ( B) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f a) + ( ap ( A) ( B) + ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( f) + (( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a) )) + ( ap-rev ( A) ( B) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( a) + ( f) + ( ( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a)) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) + ( cancel-left-path + ( B) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f a) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) + ( ( ap A B ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) a f + (( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ((coherence-is-half-adjoint-equiv A B f is-hae) a))) +``` + +Let $f : A → B$ be an equivalence between $A$ and $B$. We prove the somewhat +delicate statement that + +$$ +q = \text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) +$$ + +```rzk +#def id-conjugate-is-hae-ap-ap-is-hae + ( A B : U) + ( f : A → B) + ( a : A) + ( b : B) + ( q : (f a) = b) + (is-hae : is-half-adjoint-equiv A B f) + : q = + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) + ( b ) + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( ap ( A) ( B) ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ap ( B) ( B) ( f a) ( b) + ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) + := + concat + ((f a) = b) + ( q) -- start + ((ap B B (f a) b (identity B) q)) -- middle + ((concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) + ( b ) + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( ap ( A) ( B) ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ap ( B) ( B) ( f a) ( b) + ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) -- end + (rev + (f a = b) + ( ap B B (f a) b (identity B) q) + ( q) + (ap-id B (f a) b q ))-- path 1 + (eq-top-cancel-commutative-square' + ( B) + (f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) --w + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) --y + ( b) -- z + (ap ( A) ( B) + ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + ( rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) -- q + (ap ( B) ( B) ( f a) ( b) + (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))-- s + ( ap B B (f a) b (identity B) q ) --- r + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) --- t + (rev-nat-htpy ( B) ( B) + ( \ x → f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (x))) + ( identity B) + ( section-htpy-is-half-adjoint-equiv A B f is-hae) + ( f a) + ( b) + ( q)) + ( ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae A B f a b q is-hae)) +``` From 0d5bc6274f6d3327e42bb030a2197580eaacf071 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sat, 14 Oct 2023 21:34:12 -0700 Subject: [PATCH 07/25] one more utility in paths, reversing a previous utility --- src/hott/01-paths.rzk.md | 63 +++++++++++++++++++++++++++------------- 1 file changed, 43 insertions(+), 20 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index a5e5e6f8..c1de42b5 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -388,8 +388,7 @@ A special case of this is sometimes useful (x y : A) (p q : x = y) : (p = q) → ( concat A y x y (rev A x y q) p) = refl - := \ α → - triangle-rotation A x y y p q refl α + := triangle-rotation A x y y p q refl ``` @@ -1072,41 +1071,41 @@ triple compostion for ease of use in a later proof. := (concat (v = z) - ( r ) + ( r) ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t) ) + ( concat A v w z p (concat A w y z s t)) (rev (v = z) - (concat A v v z refl r ) + (concat A v v z refl r) ( r ) (left-unit-concat A v z r)) (concat ( v = z) ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) + ( concat A v v z (concat A v w v p q) r) ( concat A v w z p (concat A w y z s t )) (rev ( v = z ) - (concat A v v z (concat A v w v p q) r ) + (concat A v v z (concat A v w v p q) r) (concat A v v z refl r) ( concat-eq-left ( A) ( v) ( v) ( z) - ( concat A v w v p q ) + ( concat A v w v p q) ( refl ) ( H') ( r) )) ( concat ( v = z) ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w v z q r)) ( concat A v w z p (concat A w y z s t)) ( associative-concat A v w v z p q r) ( concat-eq-right - ( A ) - ( v ) + ( A) + ( v) ( w) ( z) ( p) @@ -1115,17 +1114,19 @@ triple compostion for ease of use in a later proof. ( H))))) ``` +It is also convenient to have a a version with the opposite associativity. + ```rzk #def eq-top-cancel-commutative-square' - (A : U) - (v w y z : A) - (p : v = w) - (q : w = v) - (s : w = y) - (r : v = z) - (t : y = z) - (H : (concat A w v z q r) = (concat A w y z s t)) - (H' : (concat A v w v p q) = refl) + ( A : U) + ( v w y z : A) + ( p : v = w) + ( q : w = v) + ( s : w = y) + ( r : v = z) + ( t : y = z) + ( H : (concat A w v z q r) = (concat A w y z s t)) + ( H' : (concat A v w v p q) = refl) : r = ( concat A v y z (concat A v w y p s) t) := (concat @@ -1179,6 +1180,28 @@ triple compostion for ease of use in a later proof. ( rev-associative-concat A v w y z p s t)) ``` +And a reversed version. + +```rzk +#def rev-eq-top-cancel-commutative-square' + ( A : U) + ( v w y z : A) + ( p : v = w) + ( q : w = v) + ( s : w = y) + ( r : v = z) + ( t : y = z) + ( H : (concat A w v z q r) = (concat A w y z s t)) + ( H' : (concat A v w v p q) = refl) + : ( concat A v y z (concat A v w y p s) t) = r + := + rev + ( v = z) + ( r) + ( concat A v y z (concat A v w y p s) t) + ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') +``` + From 04a937533437655731ca0b99a05da8a72b11821b Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sun, 15 Oct 2023 07:42:15 -0700 Subject: [PATCH 08/25] minor edits to the utilities --- src/hott/04-half-adjoint-equivalences.rzk.md | 53 ++++++++++++-------- 1 file changed, 32 insertions(+), 21 deletions(-) diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index e8489163..ba17132d 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -807,6 +807,9 @@ have equivalent identity types by showing that equivalences are embeddings. ## Some further useful coherences +We prove some further coherences from half-adjoint equivalences. Some of the +lemmas below resemble lemmas from the section on embeddings. + For a half-adjoint equivalence $f$ with inverse $g$ and coherence $G ⋅ f ∼ \text{ap}_f ⋅ H$ we show @@ -878,13 +881,26 @@ reversals. ( ((coherence-is-half-adjoint-equiv A B f is-hae) a))) ``` -Let $f : A → B$ be an equivalence between $A$ and $B$. We prove the somewhat -delicate statement that +Let $f : A → B$ be an equivalence between $A$ and $B$. We prove that + +$$ +\text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) = q +$$ + +This expresses a relatively natural statement that if we start with +$q: f (a) = b$, apply $g$ to get $\text{ap}_g (q) : g (f (a)) = g(b)$, +precompose with $H (a)$ to get $$ -q = \text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) +a = g(f(a)) = g(b) $$ +apply $g$ and then postcompose with $G : f (g (b)) = b$, the resulting path +$f(a) = b$ is equal to $q$. + +An alternate proof could use `triple-concat-eq-first` and +`triple-concat-nat-htpy`. The proofs do not end up much shorter. + ```rzk #def id-conjugate-is-hae-ap-ap-is-hae ( A B : U) @@ -893,8 +909,7 @@ $$ ( b : B) ( q : (f a) = b) (is-hae : is-half-adjoint-equiv A B f) - : q = - (concat ( B) + :(concat ( B) ( f a) ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) ( b ) @@ -912,12 +927,10 @@ $$ ( ap ( B) ( B) ( f a) ( b) ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))) - ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) = q := concat ((f a) = b) - ( q) -- start - ((ap B B (f a) b (identity B) q)) -- middle ((concat ( B) ( f a) ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) @@ -936,18 +949,15 @@ $$ ( ap ( B) ( B) ( f a) ( b) ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))) - ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) -- end - (rev - (f a = b) - ( ap B B (f a) b (identity B) q) - ( q) - (ap-id B (f a) b q ))-- path 1 - (eq-top-cancel-commutative-square' + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) + ((ap B B (f a) b (identity B) q)) + ( q) + (rev-eq-top-cancel-commutative-square' ( B) (f a) - ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) --w - ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) --y - ( b) -- z + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( b) (ap ( A) ( B) ( a) ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) @@ -956,12 +966,12 @@ $$ ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) ( a) ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) - ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) -- q + ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) (ap ( B) ( B) ( f a) ( b) (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))-- s - ( ap B B (f a) b (identity B) q ) --- r - ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) --- t + ( ap B B (f a) b (identity B) q ) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) (rev-nat-htpy ( B) ( B) ( \ x → f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (x))) ( identity B) @@ -970,4 +980,5 @@ $$ ( b) ( q)) ( ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae A B f a b q is-hae)) + (ap-id B (f a) b q ) ``` From 0cb0e8748bdde592bfdeff21d2aac77b267861e1 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sun, 15 Oct 2023 07:51:41 -0700 Subject: [PATCH 09/25] more edits --- src/hott/02-homotopies.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index aeb2840c..2cccca6d 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -67,7 +67,7 @@ There is also a dependent version of homotopy. ## Some path algebra for homotopies -This section contains some lemmas on the groupoidal structure of homotopies. +In this section we prove some lemmas on the groupoidal structure of homotopies. Given a homotopy between two homotopies $C : H \sim K$ this produces a homotopy $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ @@ -84,7 +84,7 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) (refl-htpy A B g) := \ x → - cancel-left-path (B) (f x) (g x) (H x) (K x) (C x) + cancel-left-path B (f x) (g x) (H x) (K x) (C x) ``` ## Whiskering homotopies @@ -155,7 +155,7 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ( p) ``` -It is sometimes useful to have this reverse +It is sometimes useful to have this in inverse form. ```rzk #def rev-nat-htpy From 214abd153fc83d3f02c42822a5372bd9b848ce54 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Wed, 11 Oct 2023 18:44:13 -0700 Subject: [PATCH 10/25] begin work on some homotopy coherences --- src/hott/01-paths.rzk.md | 13 ++++++++++ src/hott/02-homotopies.rzk.md | 48 +++++++++++++++++++++++++++++++++++ 2 files changed, 61 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index ac43faf0..fa636f5a 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -380,6 +380,19 @@ The following needs to be outside the previous section because of the usage of ( concat-concat' A x y z q r))) ``` +A special case of this is sometimes useful + +```rzk +#def cancel-left-path + (A : U) + (x y : A) + (p q : x = y) + : (p = q) → ( concat A y x y (rev A x y q) p) = refl + := \ α → + triangle-rotation A x y y p q refl α + +``` + ### Concatenation with a path and its reversal ```rzk diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index 70132dd9..c44c7237 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -41,10 +41,58 @@ This is a literate `rzk` file: Homotopy composition is defined in diagrammatic order like `#!rzk concat` but unlike composition. +The following is the unit for compositions of homotopies. + +```rzk +#def refl-htpy + (f : A → B) + : homotopy f f + := \ x → refl +``` + ```rzk #end homotopies ``` +There is also a dependent version of homotopy. + +```rzk +#def dependent-homotopy + ( A : U) + ( B : A → U) + (f g : (a : A) → B a) + : U + := (a : A) → (f a = g a) +``` + +## Some path algebra for homotopies + +This section contains some lemmas on the groupoidal structure of homotopies. + +Given a homotopy between two homotopies $C : H \sim K$ this produces a homotopy +$K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ + +```rzk +#def htpy-cancel-left + (A B : U) + (f g : A → B) + (H K : homotopy A B f g) + (C : dependent-homotopy A (\ a → f a = g a) H K) + : dependent-homotopy + A + (\ b → g b = g b) + (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) + (refl-htpy A B g) + := \ x → + cancel-left-path + (B) + (f x) + (g x) + (H x) + (K x) + (C x) +``` + ## Whiskering homotopies ```rzk From 15219fefbefc074cac46b127fc92fc49e22fd7a7 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Wed, 11 Oct 2023 20:36:27 -0700 Subject: [PATCH 11/25] added the eq-top-cancel function --- src/hott/01-paths.rzk.md | 64 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index fa636f5a..b1c4ce42 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -965,3 +965,67 @@ The following is the same as above but with alternating arguments. ( r) ( H) ``` + +The function below represents a somewhat special situation, which nevertheless +arises when dealing with certain naturality diagrams. One has a commutative +square and a path that cancels that top path. Then the type below witnesses the +equivalence between the right side of the square and a particular zig-zag of +paths. + +```rzk +#def eq-top-cancel-commutative-square + (A : U) + (v w y z : A) + (p : v = w) + (q : w = v) + (s : w = y) + (r : v = z) + (t : y = z) + (H : (concat A w v z q r) = (concat A w y z s t)) + (H' : (concat A v w v p q) = refl) + : r = (concat A v w z p (concat A w y z s t)) + := + (concat + (v = z) + ( r ) + ( concat A v v z refl r) + ( concat A v w z p (concat A w y z s t) ) + (rev + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + (concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev + ( v = z ) + (concat A v v z (concat A v w v p q) r ) + (concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) +``` From 20728fdf41706c464c5eaa5b2d668267900aacd7 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Thu, 12 Oct 2023 15:56:53 -0700 Subject: [PATCH 12/25] added an svg commutative diagram --- src/hott/01-paths.rzk.md | 88 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 86 insertions(+), 2 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index b1c4ce42..1fd50a91 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -969,8 +969,92 @@ The following is the same as above but with alternating arguments. The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the -equivalence between the right side of the square and a particular zig-zag of -paths. +equivalence between the right side of the square (in blue) and a particular +zig-zag of paths, the red zig-zag. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def eq-top-cancel-commutative-square From 2908099115c920f4cf60e63ee5466e56116af8d1 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Fri, 13 Oct 2023 16:29:00 -0700 Subject: [PATCH 13/25] added a utility for path coherence --- src/hott/01-paths.rzk.md | 204 +++++++++++++++++++++------------------ 1 file changed, 112 insertions(+), 92 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index 1fd50a91..e023b629 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -975,86 +975,86 @@ zig-zag of paths, the red zig-zag. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def eq-top-cancel-commutative-square @@ -1080,11 +1080,11 @@ zig-zag of paths, the red zig-zag. ( r ) (left-unit-concat A v z r)) (concat - ( v = z) - ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v w z p (concat A w y z s t )) - (rev + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev ( v = z ) (concat A v v z (concat A v w v p q) r ) (concat A v v z refl r) @@ -1097,13 +1097,13 @@ zig-zag of paths, the red zig-zag. ( refl ) ( H') ( r) )) - ( concat - ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) - ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right ( A ) ( v ) ( w) @@ -1113,3 +1113,23 @@ zig-zag of paths, the red zig-zag. ( concat A w y z s t) ( H))))) ``` + +```rzk + +#def htpy-id-cancel-left-concat-left-eq + (A : U) + (a b : A) + (p : a = b) + (q : a = b) + (H : p = q) + (r : b = a) + (H' : (concat A a b a q r) = refl) + : (concat A a b a p r) = refl + := concat + ( a = a) + ( concat A a b a p r ) -- begin + ( concat A a b a q r ) -- middle + ( refl ) -- end + ( concat-eq-left A a b a p q H r) + ( H' ) +``` From ca49b7d544e356e4bc07ae37da1b4555b32dd27d Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Fri, 13 Oct 2023 16:35:08 -0700 Subject: [PATCH 14/25] added commutative diagram for new utility --- src/hott/01-paths.rzk.md | 66 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index e023b629..d1bfb2ba 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -1114,6 +1114,72 @@ zig-zag of paths, the red zig-zag. ( H))))) ``` + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def htpy-id-cancel-left-concat-left-eq From 5de415fddad23665744893402c6bbde6cb86997f Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sat, 14 Oct 2023 20:49:13 -0700 Subject: [PATCH 15/25] some complicated coherences added --- src/hott/01-paths.rzk.md | 142 ++++++++++++---- src/hott/02-homotopies.rzk.md | 36 ++-- src/hott/04-half-adjoint-equivalences.rzk.md | 167 +++++++++++++++++++ 3 files changed, 296 insertions(+), 49 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index d1bfb2ba..a5e5e6f8 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -970,7 +970,8 @@ The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the equivalence between the right side of the square (in blue) and a particular -zig-zag of paths, the red zig-zag. +zig-zag of paths, the red zig-zag. We choose the assocativity order for the +triple compostion for ease of use in a later proof. @@ -1070,48 +1071,112 @@ zig-zag of paths, the red zig-zag. : r = (concat A v w z p (concat A w y z s t)) := (concat - (v = z) - ( r ) - ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t) ) - (rev (v = z) - (concat A v v z refl r ) ( r ) - (left-unit-concat A v z r)) - (concat - ( v = z) ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v w z p (concat A w y z s t )) + ( concat A v w z p (concat A w y z s t) ) (rev - ( v = z ) - (concat A v v z (concat A v w v p q) r ) - (concat A v v z refl r) - ( concat-eq-left - ( A) - ( v) - ( v) - ( z) - ( concat A v w v p q ) - ( refl ) - ( H') - ( r) )) - ( concat + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + (concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + (rev + ( v = z ) + (concat A v v z (concat A v w v p q) r ) + (concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) +``` + +```rzk +#def eq-top-cancel-commutative-square' + (A : U) + (v w y z : A) + (p : v = w) + (q : w = v) + (s : w = y) + (r : v = z) + (t : y = z) + (H : (concat A w v z q r) = (concat A w y z s t)) + (H' : (concat A v w v p q) = refl) + : r = ( concat A v y z (concat A v w y p s) t) + := + (concat ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) + ( r) ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right - ( A ) - ( v ) - ( w) - ( z) - ( p) - ( concat A w v z q r) - ( concat A w y z s t) - ( H))))) + ( concat A v y z (concat A v w y p s) t) + ( concat + ( v = z) + ( r ) + ( concat A v v z refl r) + ( concat A v w z p (concat A w y z s t) ) + ( rev + (v = z) + (concat A v v z refl r ) + ( r ) + (left-unit-concat A v z r)) + ( concat + ( v = z) + ( concat A v v z refl r) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v w z p (concat A w y z s t )) + ( rev + ( v = z ) + ( concat A v v z (concat A v w v p q) r ) + ( concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q ) + ( refl ) + ( H') + ( r) )) + ( concat + ( v = z) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A ) + ( v ) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) + ( rev-associative-concat A v w y z p s t)) ``` @@ -1180,6 +1245,9 @@ zig-zag of paths, the red zig-zag. +If $H \sim K$ is a homotopy between homotopies, then we can cancel on the left +to get $$ K^{-1} \cdot H \sim \texttt{refl}$$ + ```rzk #def htpy-id-cancel-left-concat-left-eq diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index c44c7237..aeb2840c 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -74,23 +74,17 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ```rzk #def htpy-cancel-left - (A B : U) - (f g : A → B) - (H K : homotopy A B f g) - (C : dependent-homotopy A (\ a → f a = g a) H K) - : dependent-homotopy + (A B : U) + (f g : A → B) + (H K : homotopy A B f g) + (C : dependent-homotopy A (\ a → f a = g a) H K) + : dependent-homotopy A (\ b → g b = g b) (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) (refl-htpy A B g) := \ x → - cancel-left-path - (B) - (f x) - (g x) - (H x) - (K x) - (C x) + cancel-left-path (B) (f x) (g x) (H x) (K x) (C x) ``` ## Whiskering homotopies @@ -161,6 +155,24 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ( p) ``` +It is sometimes useful to have this reverse + +```rzk +#def rev-nat-htpy + ( A B : U) + ( f g : A → B) + ( H : homotopy A B f g) + ( x y : A) + ( p : x = y) + : ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) = + ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) + := rev + ( f x = g y) + ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) + ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) + ( nat-htpy A B f g H x y p) +``` + ```rzk title="Naturality in another form" #def triple-concat-nat-htpy ( A B : U) diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index b26e911f..e8489163 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -804,3 +804,170 @@ have equivalent identity types by showing that equivalences are embeddings. : Equiv (x = y) (f x = f y) := (ap A B x y f , is-emb-is-equiv A B f is-equiv-f x y) ``` + +## Some further useful coherences + +For a half-adjoint equivalence $f$ with inverse $g$ and coherence +$G ⋅ f ∼ \text{ap}_f ⋅ H$ we show + +$$ +\text{ap}_f (H^{-1} a) ⋅ G (f a) = \texttt{refl}_{f (a)}. +$$ + +This is a consequence of cancelling the coherence on the left, and then applying +the equality $\text{ap}_f (H^{-1} a) = (\text{ap}_f (H a))^{-1}$. It is +cumbersome to state and prove only becaues of data revtrieval and the number of +reversals. + +```rzk +#def ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae + (A B : U) + (f : A → B) + (a : A) + (b : B) + (q : (f a) = b) + (is-hae : is-half-adjoint-equiv A B f) + : (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a ))) + ( f a) + (ap ( A) ( B) + ( a) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) ( f a))) + ( f) + ( rev ( A) + ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ((retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a))) + = refl + := + htpy-id-cancel-left-concat-left-eq + ( B) + (f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( ap ( A) ( B) + ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) ( f a))) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( rev ( B) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f a) + ( ap ( A) ( B) + ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( f) + (( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a) )) + ( ap-rev ( A) ( B) + (((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( a) + ( f) + ( ( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a)) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) + ( cancel-left-path + ( B) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f a) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) + ( ( ap A B ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) a f + (( retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ((coherence-is-half-adjoint-equiv A B f is-hae) a))) +``` + +Let $f : A → B$ be an equivalence between $A$ and $B$. We prove the somewhat +delicate statement that + +$$ +q = \text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) +$$ + +```rzk +#def id-conjugate-is-hae-ap-ap-is-hae + ( A B : U) + ( f : A → B) + ( a : A) + ( b : B) + ( q : (f a) = b) + (is-hae : is-half-adjoint-equiv A B f) + : q = + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) + ( b ) + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( ap ( A) ( B) ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ap ( B) ( B) ( f a) ( b) + ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) + := + concat + ((f a) = b) + ( q) -- start + ((ap B B (f a) b (identity B) q)) -- middle + ((concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) + ( b ) + (concat ( B) + ( f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( ap ( A) ( B) ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + (rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ( ap ( B) ( B) ( f a) ( b) + ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) -- end + (rev + (f a = b) + ( ap B B (f a) b (identity B) q) + ( q) + (ap-id B (f a) b q ))-- path 1 + (eq-top-cancel-commutative-square' + ( B) + (f a) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) --w + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) --y + ( b) -- z + (ap ( A) ( B) + ( a) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( f) + ( rev ( A) + ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) + ( a) + ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) + ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) -- q + (ap ( B) ( B) ( f a) ( b) + (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) + ( q))-- s + ( ap B B (f a) b (identity B) q ) --- r + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) --- t + (rev-nat-htpy ( B) ( B) + ( \ x → f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (x))) + ( identity B) + ( section-htpy-is-half-adjoint-equiv A B f is-hae) + ( f a) + ( b) + ( q)) + ( ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae A B f a b q is-hae)) +``` From bd23aa559ade32c07e13dd33e168ba980db92d96 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sat, 14 Oct 2023 21:34:12 -0700 Subject: [PATCH 16/25] one more utility in paths, reversing a previous utility --- src/hott/01-paths.rzk.md | 63 +++++++++++++++++++++++++++------------- 1 file changed, 43 insertions(+), 20 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index a5e5e6f8..c1de42b5 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -388,8 +388,7 @@ A special case of this is sometimes useful (x y : A) (p q : x = y) : (p = q) → ( concat A y x y (rev A x y q) p) = refl - := \ α → - triangle-rotation A x y y p q refl α + := triangle-rotation A x y y p q refl ``` @@ -1072,41 +1071,41 @@ triple compostion for ease of use in a later proof. := (concat (v = z) - ( r ) + ( r) ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t) ) + ( concat A v w z p (concat A w y z s t)) (rev (v = z) - (concat A v v z refl r ) + (concat A v v z refl r) ( r ) (left-unit-concat A v z r)) (concat ( v = z) ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) + ( concat A v v z (concat A v w v p q) r) ( concat A v w z p (concat A w y z s t )) (rev ( v = z ) - (concat A v v z (concat A v w v p q) r ) + (concat A v v z (concat A v w v p q) r) (concat A v v z refl r) ( concat-eq-left ( A) ( v) ( v) ( z) - ( concat A v w v p q ) + ( concat A v w v p q) ( refl ) ( H') ( r) )) ( concat ( v = z) ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) + ( concat A v w z p (concat A w v z q r)) ( concat A v w z p (concat A w y z s t)) ( associative-concat A v w v z p q r) ( concat-eq-right - ( A ) - ( v ) + ( A) + ( v) ( w) ( z) ( p) @@ -1115,17 +1114,19 @@ triple compostion for ease of use in a later proof. ( H))))) ``` +It is also convenient to have a a version with the opposite associativity. + ```rzk #def eq-top-cancel-commutative-square' - (A : U) - (v w y z : A) - (p : v = w) - (q : w = v) - (s : w = y) - (r : v = z) - (t : y = z) - (H : (concat A w v z q r) = (concat A w y z s t)) - (H' : (concat A v w v p q) = refl) + ( A : U) + ( v w y z : A) + ( p : v = w) + ( q : w = v) + ( s : w = y) + ( r : v = z) + ( t : y = z) + ( H : (concat A w v z q r) = (concat A w y z s t)) + ( H' : (concat A v w v p q) = refl) : r = ( concat A v y z (concat A v w y p s) t) := (concat @@ -1179,6 +1180,28 @@ triple compostion for ease of use in a later proof. ( rev-associative-concat A v w y z p s t)) ``` +And a reversed version. + +```rzk +#def rev-eq-top-cancel-commutative-square' + ( A : U) + ( v w y z : A) + ( p : v = w) + ( q : w = v) + ( s : w = y) + ( r : v = z) + ( t : y = z) + ( H : (concat A w v z q r) = (concat A w y z s t)) + ( H' : (concat A v w v p q) = refl) + : ( concat A v y z (concat A v w y p s) t) = r + := + rev + ( v = z) + ( r) + ( concat A v y z (concat A v w y p s) t) + ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') +``` + From 8b17ef5fa507985c9ec4544a91d63121c8fb841a Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sun, 15 Oct 2023 07:42:15 -0700 Subject: [PATCH 17/25] minor edits to the utilities --- src/hott/04-half-adjoint-equivalences.rzk.md | 53 ++++++++++++-------- 1 file changed, 32 insertions(+), 21 deletions(-) diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index e8489163..ba17132d 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -807,6 +807,9 @@ have equivalent identity types by showing that equivalences are embeddings. ## Some further useful coherences +We prove some further coherences from half-adjoint equivalences. Some of the +lemmas below resemble lemmas from the section on embeddings. + For a half-adjoint equivalence $f$ with inverse $g$ and coherence $G ⋅ f ∼ \text{ap}_f ⋅ H$ we show @@ -878,13 +881,26 @@ reversals. ( ((coherence-is-half-adjoint-equiv A B f is-hae) a))) ``` -Let $f : A → B$ be an equivalence between $A$ and $B$. We prove the somewhat -delicate statement that +Let $f : A → B$ be an equivalence between $A$ and $B$. We prove that + +$$ +\text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) = q +$$ + +This expresses a relatively natural statement that if we start with +$q: f (a) = b$, apply $g$ to get $\text{ap}_g (q) : g (f (a)) = g(b)$, +precompose with $H (a)$ to get $$ -q = \text{ap}_f (H^-1 (a)) ⋅ \text{ap}_{f ∘ g} (q) ⋅ G (b) +a = g(f(a)) = g(b) $$ +apply $g$ and then postcompose with $G : f (g (b)) = b$, the resulting path +$f(a) = b$ is equal to $q$. + +An alternate proof could use `triple-concat-eq-first` and +`triple-concat-nat-htpy`. The proofs do not end up much shorter. + ```rzk #def id-conjugate-is-hae-ap-ap-is-hae ( A B : U) @@ -893,8 +909,7 @@ $$ ( b : B) ( q : (f a) = b) (is-hae : is-half-adjoint-equiv A B f) - : q = - (concat ( B) + :(concat ( B) ( f a) ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) ( b ) @@ -912,12 +927,10 @@ $$ ( ap ( B) ( B) ( f a) ( b) ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))) - ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) = q := concat ((f a) = b) - ( q) -- start - ((ap B B (f a) b (identity B) q)) -- middle ((concat ( B) ( f a) ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (b))) @@ -936,18 +949,15 @@ $$ ( ap ( B) ( B) ( f a) ( b) ( \z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))) - ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) -- end - (rev - (f a = b) - ( ap B B (f a) b (identity B) q) - ( q) - (ap-id B (f a) b q ))-- path 1 - (eq-top-cancel-commutative-square' + ( ( section-htpy-is-half-adjoint-equiv A B f is-hae) (b))) ) + ((ap B B (f a) b (identity B) q)) + ( q) + (rev-eq-top-cancel-commutative-square' ( B) (f a) - ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) --w - ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) --y - ( b) -- z + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (f a))) + ( f ((map-inverse-is-half-adjoint-equiv A B f is-hae) b)) + ( b) (ap ( A) ( B) ( a) ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) @@ -956,12 +966,12 @@ $$ ( (map-inverse-is-half-adjoint-equiv A B f is-hae) (f a)) ( a) ( (retraction-htpy-is-half-adjoint-equiv A B f is-hae) a))) - ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) -- q + ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) (ap ( B) ( B) ( f a) ( b) (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) ( q))-- s - ( ap B B (f a) b (identity B) q ) --- r - ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) --- t + ( ap B B (f a) b (identity B) q ) + ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) (rev-nat-htpy ( B) ( B) ( \ x → f ((map-inverse-is-half-adjoint-equiv A B f is-hae) (x))) ( identity B) @@ -970,4 +980,5 @@ $$ ( b) ( q)) ( ap-rev-retr-htpy-concat-sec-htpy-is-refl-is-hae A B f a b q is-hae)) + (ap-id B (f a) b q ) ``` From 1cedae0508f22b90240fbd6b97d9c749d37ec2ee Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sun, 15 Oct 2023 07:51:41 -0700 Subject: [PATCH 18/25] more edits --- src/hott/02-homotopies.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index aeb2840c..2cccca6d 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -67,7 +67,7 @@ There is also a dependent version of homotopy. ## Some path algebra for homotopies -This section contains some lemmas on the groupoidal structure of homotopies. +In this section we prove some lemmas on the groupoidal structure of homotopies. Given a homotopy between two homotopies $C : H \sim K$ this produces a homotopy $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ @@ -84,7 +84,7 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) (refl-htpy A B g) := \ x → - cancel-left-path (B) (f x) (g x) (H x) (K x) (C x) + cancel-left-path B (f x) (g x) (H x) (K x) (C x) ``` ## Whiskering homotopies @@ -155,7 +155,7 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ ( p) ``` -It is sometimes useful to have this reverse +It is sometimes useful to have this in inverse form. ```rzk #def rev-nat-htpy From ae6c231edda89c67146f0d4b3e8897b64767de81 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Sun, 15 Oct 2023 12:33:35 -0700 Subject: [PATCH 19/25] dependent-homotopy to dhomotopy --- src/hott/02-homotopies.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index 2cccca6d..8615e067 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -57,7 +57,7 @@ The following is the unit for compositions of homotopies. There is also a dependent version of homotopy. ```rzk -#def dependent-homotopy +#def dhomotopy ( A : U) ( B : A → U) (f g : (a : A) → B a) @@ -77,8 +77,8 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ (A B : U) (f g : A → B) (H K : homotopy A B f g) - (C : dependent-homotopy A (\ a → f a = g a) H K) - : dependent-homotopy + (C : dhomotopy A (\ a → f a = g a) H K) + : dhomotopy A (\ b → g b = g b) (\ x → concat B (g x) (f x) (g x) (rev B (f x) (g x) (K x)) (H x)) From bff77876a12e2a419fe23bb3d01733bf8fedb95c Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 26 Oct 2023 19:03:13 -0400 Subject: [PATCH 20/25] Update src/hott/01-paths.rzk.md Co-authored-by: Fredrik Bakke --- src/hott/01-paths.rzk.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index c1de42b5..d3e50b3c 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -389,7 +389,6 @@ A special case of this is sometimes useful (p q : x = y) : (p = q) → ( concat A y x y (rev A x y q) p) = refl := triangle-rotation A x y y p q refl - ``` ### Concatenation with a path and its reversal From 7c457728f47389645d871c1c5cc7a25e2e815d57 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 26 Oct 2023 19:03:29 -0400 Subject: [PATCH 21/25] Update src/hott/01-paths.rzk.md Co-authored-by: Fredrik Bakke --- src/hott/01-paths.rzk.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index d3e50b3c..d80480fe 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -1194,11 +1194,11 @@ And a reversed version. ( H' : (concat A v w v p q) = refl) : ( concat A v y z (concat A v w y p s) t) = r := - rev - ( v = z) - ( r) - ( concat A v y z (concat A v w y p s) t) - ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') + rev + ( v = z) + ( r) + ( concat A v y z (concat A v w y p s) t) + ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') ``` From ccd16567300ba1ec6f9b8f158b7b87ad3d2acaca Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 26 Oct 2023 19:03:36 -0400 Subject: [PATCH 22/25] Update src/hott/04-half-adjoint-equivalences.rzk.md Co-authored-by: Fredrik Bakke --- src/hott/04-half-adjoint-equivalences.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index ba17132d..749ad0d6 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -969,7 +969,7 @@ An alternate proof could use `triple-concat-eq-first` and ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) (ap ( B) ( B) ( f a) ( b) (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) - ( q))-- s + ( q)) ( ap B B (f a) b (identity B) q ) ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) (rev-nat-htpy ( B) ( B) From 0560d7867afe3077da03c1654ddec023ce2cbc71 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 26 Oct 2023 19:05:37 -0400 Subject: [PATCH 23/25] Update src/hott/02-homotopies.rzk.md Co-authored-by: Fredrik Bakke --- src/hott/02-homotopies.rzk.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index 8615e067..1881dde8 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -166,11 +166,12 @@ It is sometimes useful to have this in inverse form. ( p : x = y) : ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) = ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) - := rev - ( f x = g y) - ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) - ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) - ( nat-htpy A B f g H x y p) + := + rev + ( f x = g y) + ( concat B (f x) (f y) (g y) (ap A B x y f p) (H y)) + ( concat B (f x) (g x) (g y) (H x) (ap A B x y g p)) + ( nat-htpy A B f g H x y p) ``` ```rzk title="Naturality in another form" From c9c0441553187fb76d6e4c9be0cffdc0721b57b2 Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Thu, 26 Oct 2023 22:03:05 -0700 Subject: [PATCH 24/25] simplified a proof and fixed some indentation --- src/hott/01-paths.rzk.md | 82 +++++--------------- src/hott/04-half-adjoint-equivalences.rzk.md | 2 +- 2 files changed, 22 insertions(+), 62 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index c1de42b5..3a8a7970 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -1129,55 +1129,14 @@ It is also convenient to have a a version with the opposite associativity. ( H' : (concat A v w v p q) = refl) : r = ( concat A v y z (concat A v w y p s) t) := - (concat - ( v = z) - ( r) - ( concat A v w z p (concat A w y z s t)) - ( concat A v y z (concat A v w y p s) t) - ( concat - ( v = z) - ( r ) - ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t) ) - ( rev - (v = z) - (concat A v v z refl r ) - ( r ) - (left-unit-concat A v z r)) - ( concat - ( v = z) - ( concat A v v z refl r) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v w z p (concat A w y z s t )) - ( rev - ( v = z ) - ( concat A v v z (concat A v w v p q) r ) - ( concat A v v z refl r) - ( concat-eq-left - ( A) - ( v) - ( v) - ( z) - ( concat A v w v p q ) - ( refl ) - ( H') - ( r) )) - ( concat - ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r) ) - ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right - ( A ) - ( v ) - ( w) - ( z) - ( p) - ( concat A w v z q r) - ( concat A w y z s t) - ( H))))) - ( rev-associative-concat A v w y z p s t)) + concat + ( v = z) + ( r) + ( concat A v w z p (concat A w y z s t)) + ( concat A v y z (concat A v w y p s) t) + ( eq-top-cancel-commutative-square A v w y z p q s r t H H') + ( rev-associative-concat A v w y z p s t) + ``` And a reversed version. @@ -1195,11 +1154,11 @@ And a reversed version. ( H' : (concat A v w v p q) = refl) : ( concat A v y z (concat A v w y p s) t) = r := - rev - ( v = z) - ( r) - ( concat A v y z (concat A v w y p s) t) - ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') + rev + ( v = z) + ( r) + ( concat A v y z (concat A v w y p s) t) + ( eq-top-cancel-commutative-square' A v w y z p q s r t H H') ``` @@ -1282,11 +1241,12 @@ to get $$ K^{-1} \cdot H \sim \texttt{refl}$$ (r : b = a) (H' : (concat A a b a q r) = refl) : (concat A a b a p r) = refl - := concat - ( a = a) - ( concat A a b a p r ) -- begin - ( concat A a b a q r ) -- middle - ( refl ) -- end - ( concat-eq-left A a b a p q H r) - ( H' ) + := + concat + ( a = a) + ( concat A a b a p r ) + ( concat A a b a q r ) + ( refl ) + ( concat-eq-left A a b a p q H r) + ( H' ) ``` diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index ba17132d..749ad0d6 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -969,7 +969,7 @@ An alternate proof could use `triple-concat-eq-first` and ((section-htpy-is-half-adjoint-equiv A B f is-hae) (f a)) (ap ( B) ( B) ( f a) ( b) (\z → (f ((map-inverse-is-half-adjoint-equiv A B f is-hae) z))) - ( q))-- s + ( q)) ( ap B B (f a) b (identity B) q ) ( (section-htpy-is-half-adjoint-equiv A B f is-hae) b) (rev-nat-htpy ( B) ( B) From e4021a99876e0c6b9f15b726a285ab939409dfec Mon Sep 17 00:00:00 2001 From: jonalfcam Date: Thu, 26 Oct 2023 22:16:53 -0700 Subject: [PATCH 25/25] small edits around latex --- src/hott/01-paths.rzk.md | 80 ++++++++++++++++++++-------------------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index 2c604168..f1ccefbb 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -1068,49 +1068,49 @@ triple compostion for ease of use in a later proof. (H' : (concat A v w v p q) = refl) : r = (concat A v w z p (concat A w y z s t)) := - (concat + (concat + (v = z) + ( r) + ( concat A v v z refl r) + ( concat A v w z p (concat A w y z s t)) + (rev (v = z) - ( r) + (concat A v v z refl r) + ( r ) + (left-unit-concat A v z r)) + (concat + ( v = z) ( concat A v v z refl r) - ( concat A v w z p (concat A w y z s t)) + ( concat A v v z (concat A v w v p q) r) + ( concat A v w z p (concat A w y z s t )) (rev - (v = z) - (concat A v v z refl r) - ( r ) - (left-unit-concat A v z r)) - (concat + ( v = z ) + (concat A v v z (concat A v w v p q) r) + (concat A v v z refl r) + ( concat-eq-left + ( A) + ( v) + ( v) + ( z) + ( concat A v w v p q) + ( refl ) + ( H') + ( r) )) + ( concat ( v = z) - ( concat A v v z refl r) ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w y z s t )) - (rev - ( v = z ) - (concat A v v z (concat A v w v p q) r) - (concat A v v z refl r) - ( concat-eq-left - ( A) - ( v) - ( v) - ( z) - ( concat A v w v p q) - ( refl ) - ( H') - ( r) )) - ( concat - ( v = z) - ( concat A v v z (concat A v w v p q) r) - ( concat A v w z p (concat A w v z q r)) - ( concat A v w z p (concat A w y z s t)) - ( associative-concat A v w v z p q r) - ( concat-eq-right - ( A) - ( v) - ( w) - ( z) - ( p) - ( concat A w v z q r) - ( concat A w y z s t) - ( H))))) + ( concat A v w z p (concat A w v z q r)) + ( concat A v w z p (concat A w y z s t)) + ( associative-concat A v w v z p q r) + ( concat-eq-right + ( A) + ( v) + ( w) + ( z) + ( p) + ( concat A w v z q r) + ( concat A w y z s t) + ( H))))) ``` It is also convenient to have a a version with the opposite associativity. @@ -1226,8 +1226,8 @@ And a reversed version. -If $H \sim K$ is a homotopy between homotopies, then we can cancel on the left -to get $$ K^{-1} \cdot H \sim \texttt{refl}$$ +Given a homotopy between paths `#! H : p = q`, then we can cancel on the left to +get a homotopy between `#!rzk concat (rev p) q` and `#! refl`. ```rzk