From a14f20452836f943ccdc30a824973eaa88b1a3fd Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Fri, 10 Nov 2023 16:57:04 -0500 Subject: [PATCH 01/20] Define the problem and some helpers --- src/simplicial-hott/10-rezk-types.rzk.md | 53 ++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 0c426fec..064ba8e0 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -836,3 +836,56 @@ arrows. ( y) ( e) ``` + +## Representable isos + +```rzk +#def inverse-equiv-iso-representable -- helper to get the fiberwise inverse and the homotopies. this carries all the information from the equivalence + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( has-inverse ( hom A a x) ( hom A a' x) ( first ( ψ x))) + := \ x → ( has-inverse-is-equiv + ( hom A a x) + ( hom A a' x) + ( first ( ψ x)) + ( second ( ψ x))) + +#def map-equiv-iso-representable -- helper to get map in the fiberwise equiv for the specified direction + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( hom A a x) → ( hom A a' x) + := \ x → first ( ψ x) + +#def inv-map-equiv-iso-representable -- helper to get inverse of map in the fiberwise equiv for the specified direction + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( hom A a' x) → ( hom A a x) + := \ x → first ( ( inverse-equiv-iso-representable A is-segal-A a a' ψ) x) + +#def arrow-map-equiv-iso-representable -- helper to get the arrow from the + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : hom A a' a + := evid A a ( hom A a') ( map-equiv-iso-representable A is-segal-A a a' ψ) + +#def arrow-inv-map-equiv-iso-representable -- helper to get the arrow from the + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : hom A a a' + := + evid + ( A) + ( a') + ( hom A a) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) +``` From 261305640762bf3c63fb33faf4acece7a7a80979 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Fri, 10 Nov 2023 16:57:48 -0500 Subject: [PATCH 02/20] Extract homotopies --- src/simplicial-hott/10-rezk-types.rzk.md | 42 ++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 064ba8e0..9a785442 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -889,3 +889,45 @@ arrows. ( hom A a) ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) ``` +We now show that `arrow-map-equiv-iso-representable` has a retraction + `arrow-inv-map-equiv-iso-representable` + +```rzk +#def htpy-comp-inv-map-equiv-map-equiv-iso-representable --homotopy for a one composition + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( homotopy + ( hom A a x) + ( hom A a x) + ( comp + ( hom A a x) + ( hom A a' x) + ( hom A a x) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x) + ( map-equiv-iso-representable A is-segal-A a a' ψ x)) + ( identity ( hom A a x))) + := + \ x + → first ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) + +#def htpy-comp-map-equiv-inv-map-equiv-iso-representable --homotopy for a other composition + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( homotopy + ( hom A a' x) + ( hom A a' x) + ( comp + ( hom A a' x) + ( hom A a x) + ( hom A a' x) + ( map-equiv-iso-representable A is-segal-A a a' ψ x) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x)) + ( identity ( hom A a' x))) + := + \ x + → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) +``` From 7e1ebaa8bb10778d69f9393344e7115cc6c80d42 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 13 Nov 2023 18:34:02 -0500 Subject: [PATCH 03/20] define all paths --- src/simplicial-hott/10-rezk-types.rzk.md | 308 ++++++++++++++++++++++- 1 file changed, 301 insertions(+), 7 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 9a785442..57d72058 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -840,7 +840,7 @@ arrows. ## Representable isos ```rzk -#def inverse-equiv-iso-representable -- helper to get the fiberwise inverse and the homotopies. this carries all the information from the equivalence +#def inverse-equiv-iso-representable ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -852,7 +852,7 @@ arrows. ( first ( ψ x)) ( second ( ψ x))) -#def map-equiv-iso-representable -- helper to get map in the fiberwise equiv for the specified direction +#def map-equiv-iso-representable ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -860,7 +860,7 @@ arrows. : ( x : A) → ( hom A a x) → ( hom A a' x) := \ x → first ( ψ x) -#def inv-map-equiv-iso-representable -- helper to get inverse of map in the fiberwise equiv for the specified direction +#def inv-map-equiv-iso-representable ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -868,7 +868,7 @@ arrows. : ( x : A) → ( hom A a' x) → ( hom A a x) := \ x → first ( ( inverse-equiv-iso-representable A is-segal-A a a' ψ) x) -#def arrow-map-equiv-iso-representable -- helper to get the arrow from the +#def arrow-map-equiv-iso-representable ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -876,7 +876,7 @@ arrows. : hom A a' a := evid A a ( hom A a') ( map-equiv-iso-representable A is-segal-A a a' ψ) -#def arrow-inv-map-equiv-iso-representable -- helper to get the arrow from the +#def arrow-inv-map-equiv-iso-representable ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -893,7 +893,7 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction `arrow-inv-map-equiv-iso-representable` ```rzk -#def htpy-comp-inv-map-equiv-map-equiv-iso-representable --homotopy for a one composition +#def htpy-comp-inv-map-equiv-map-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -912,7 +912,7 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction \ x → first ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) -#def htpy-comp-map-equiv-inv-map-equiv-iso-representable --homotopy for a other composition +#def htpy-comp-map-equiv-inv-map-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -930,4 +930,298 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction := \ x → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) + +#def compute-htpy-comp-map-equiv-inv-map-equiv + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : map-equiv-iso-representable A is-segal-A a a' ψ a' + ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( id-hom A a')) + = id-hom A a' + := htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ a' ( id-hom A a') + +#def compute-htpy-comp-inv-map-equiv-map-equiv -- p1 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) ( id-hom A a)) + = id-hom A a + := htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ a ( id-hom A a) + +#def eq-inv-map-equiv-arrow-maps-equiv --p2 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + ( id-hom A a)) + = + inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + := + ap + ( hom A a' a) + ( hom A a a) + ( map-equiv-iso-representable A is-segal-A a a' ψ a ( id-hom A a)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a) + ( eq-compute-precomposition-evid + ( funext) + ( A) + ( is-segal-A) + ( a) + ( a') + ( map-equiv-iso-representable A is-segal-A a a' ψ) + ( a) + ( id-hom A a)) + +#def eq-inv-map-equiv-arrow-maps-equiv2 --p3 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + = + comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + := + eq-compute-precomposition-evid + ( funext) + ( A) + ( is-segal-A) + ( a') + ( a) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + +#def eq-inv-map-equiv-arrow-maps-equiv3 --p4 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( id-hom A a) + = + comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) + := + associative-is-segal + ( extext) + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a) + +#def eq-inv-map-equiv-arrow-maps-equiv4 --p5 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( id-hom A a) + = + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + := + comp-id-is-segal + ( A) + ( is-segal-A) + ( a) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) ``` From 48fc8979bd66f2bb6d05972db1bd0f73a903badc Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Sat, 18 Nov 2023 15:52:45 -0500 Subject: [PATCH 04/20] path for section --- src/simplicial-hott/10-rezk-types.rzk.md | 226 ++++++++++++++++++++++- 1 file changed, 225 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 57d72058..3df0994a 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -952,7 +952,7 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction = id-hom A a := htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ a ( id-hom A a) -#def eq-inv-map-equiv-arrow-maps-equiv --p2 +#def eq-inv-map-equiv-arrow-maps-equiv1 --p2 ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1224,4 +1224,228 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction ( a) ( a') ( ψ))) + +#def section-arrow-map-equiv-iso-representable2 uses ( extext funext) + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + = id-hom A a + := + quintuple-concat + ( hom A a a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( id-hom A a)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a))) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a))) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + ( id-hom A a))) + ( id-hom A a) + ( rev + ( hom A a a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a) + ( a) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( id-hom A a)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( eq-inv-map-equiv-arrow-maps-equiv4 A is-segal-A a a' ψ)) + ( eq-inv-map-equiv-arrow-maps-equiv3 A is-segal-A a a' ψ) + ( rev + ( hom A a a) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a))) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a) + ( arrow-inv-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a)) ) + ( eq-inv-map-equiv-arrow-maps-equiv2 A is-segal-A a a' ψ)) + ( rev + ( hom A a a) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + ( id-hom A a))) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a) + ( arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) + ( id-hom A a))) + ( eq-inv-map-equiv-arrow-maps-equiv1 A is-segal-A a a' ψ)) + ( compute-htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ) ``` From edc1bf592b6a229c63ac1de4c89d04e1a85d1814 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Sat, 18 Nov 2023 16:25:27 -0500 Subject: [PATCH 05/20] the section --- src/simplicial-hott/10-rezk-types.rzk.md | 49 ++++++++++++++++-------- 1 file changed, 34 insertions(+), 15 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 3df0994a..6ec62ede 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -837,7 +837,7 @@ arrows. ( e) ``` -## Representable isos +## Representable isomorphisms. ```rzk #def inverse-equiv-iso-representable @@ -889,8 +889,8 @@ arrows. ( hom A a) ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) ``` -We now show that `arrow-map-equiv-iso-representable` has a retraction - `arrow-inv-map-equiv-iso-representable` +We now show that `arrow-map-equiv-iso-representable` section + `arrow-inv-map-equiv-iso-representable`. ```rzk #def htpy-comp-inv-map-equiv-map-equiv @@ -930,18 +930,10 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction := \ x → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) +``` +We compute the required paths for the section of `#rzk arrow-map-iso-representable`. -#def compute-htpy-comp-map-equiv-inv-map-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-equiv-iso-representable A is-segal-A a a' ψ a' - ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') - ( id-hom A a')) - = id-hom A a' - := htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ a' ( id-hom A a') - +```rzk #def compute-htpy-comp-inv-map-equiv-map-equiv -- p1 ( A : U) ( is-segal-A : is-segal A) @@ -1224,8 +1216,11 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction ( a) ( a') ( ψ))) +``` +Concatenate all the paths above. -#def section-arrow-map-equiv-iso-representable2 uses ( extext funext) +```rzk +#def eq-comp-arrow-inv-map-arrow-map-equiv-iso-representable uses (extext funext) ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1449,3 +1444,27 @@ We now show that `arrow-map-equiv-iso-representable` has a retraction ( eq-inv-map-equiv-arrow-maps-equiv1 A is-segal-A a a' ψ)) ( compute-htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ) ``` + +Now we give the section of `arrow-map-equiv-iso-representable`. + +```rzk +#def section-arrow-map-iso-representable uses ( extext funext) + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : Section-arrow + ( A) + ( is-segal-A) + ( a') + ( a) + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + := + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ + , eq-comp-arrow-inv-map-arrow-map-equiv-iso-representable + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) +``` From cd48607d4f02480692028c58d3df512b3c7ecd00 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Sun, 19 Nov 2023 17:16:26 -0500 Subject: [PATCH 06/20] eddit names --- src/simplicial-hott/10-rezk-types.rzk.md | 66 +++++++++++++----------- 1 file changed, 36 insertions(+), 30 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 6ec62ede..1fd7ff51 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -889,8 +889,9 @@ arrows. ( hom A a) ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) ``` + We now show that `arrow-map-equiv-iso-representable` section - `arrow-inv-map-equiv-iso-representable`. +`arrow-inv-map-equiv-iso-representable`. ```rzk #def htpy-comp-inv-map-equiv-map-equiv @@ -911,30 +912,13 @@ We now show that `arrow-map-equiv-iso-representable` section := \ x → first ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) - -#def htpy-comp-map-equiv-inv-map-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : ( x : A) → ( homotopy - ( hom A a' x) - ( hom A a' x) - ( comp - ( hom A a' x) - ( hom A a x) - ( hom A a' x) - ( map-equiv-iso-representable A is-segal-A a a' ψ x) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x)) - ( identity ( hom A a' x))) - := - \ x - → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) ``` -We compute the required paths for the section of `#rzk arrow-map-iso-representable`. + +We compute the required paths for the section of +`arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-inv-map-equiv-map-equiv -- p1 +#def compute-htpy-comp-inv-map-equiv-map-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -944,7 +928,7 @@ We compute the required paths for the section of `#rzk arrow-map-iso-representab = id-hom A a := htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ a ( id-hom A a) -#def eq-inv-map-equiv-arrow-maps-equiv1 --p2 +#def eq-inv-map-map-equiv-iso-inv-map-comp-arrow-map-idhom-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -996,7 +980,7 @@ We compute the required paths for the section of `#rzk arrow-map-iso-representab ( a) ( id-hom A a)) -#def eq-inv-map-equiv-arrow-maps-equiv2 --p3 +#def eq-inv-map-comp-arr-map-equiv-comp-arrow-inv-map-equiv-comp-arr-map-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1064,7 +1048,7 @@ We compute the required paths for the section of `#rzk arrow-map-iso-representab ( ψ)) ( id-hom A a)) -#def eq-inv-map-equiv-arrow-maps-equiv3 --p4 +#def eq-comp-comp-arrow-inv-map-arr-map-comp-arr-inv-map-comp-arr-map-idhom-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1143,7 +1127,7 @@ We compute the required paths for the section of `#rzk arrow-map-iso-representab ( ψ)) ( id-hom A a) -#def eq-inv-map-equiv-arrow-maps-equiv4 --p5 +#def eq-comp-comp-inv-map-equiv-arr-map-idhom-a-comp-arr-inv-map-arr-map ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1217,6 +1201,7 @@ We compute the required paths for the section of `#rzk arrow-map-iso-representab ( a') ( ψ))) ``` + Concatenate all the paths above. ```rzk @@ -1378,8 +1363,18 @@ Concatenate all the paths above. ( a) ( a') ( ψ))) - ( eq-inv-map-equiv-arrow-maps-equiv4 A is-segal-A a a' ψ)) - ( eq-inv-map-equiv-arrow-maps-equiv3 A is-segal-A a a' ψ) + ( eq-comp-comp-inv-map-equiv-arr-map-idhom-a-comp-arr-inv-map-arr-map + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( eq-comp-comp-arrow-inv-map-arr-map-comp-arr-inv-map-comp-arr-map-idhom-a + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) ( rev ( hom A a a) ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a @@ -1421,7 +1416,12 @@ Concatenate all the paths above. ( a') ( ψ)) ( id-hom A a)) ) - ( eq-inv-map-equiv-arrow-maps-equiv2 A is-segal-A a a' ψ)) + ( eq-inv-map-comp-arr-map-equiv-comp-arrow-inv-map-equiv-comp-arr-map-equiv + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) ( rev ( hom A a a) ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a @@ -1441,7 +1441,12 @@ Concatenate all the paths above. ( a') ( ψ)) ( id-hom A a))) - ( eq-inv-map-equiv-arrow-maps-equiv1 A is-segal-A a a' ψ)) + ( eq-inv-map-map-equiv-iso-inv-map-comp-arrow-map-idhom-a + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) ( compute-htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ) ``` @@ -1468,3 +1473,4 @@ Now we give the section of `arrow-map-equiv-iso-representable`. ( a') ( ψ)) ``` + From f7530c9b64f88db161b7dc811e8b02ed86c41a05 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Sun, 19 Nov 2023 23:18:56 -0500 Subject: [PATCH 07/20] give the retraction --- src/simplicial-hott/10-rezk-types.rzk.md | 272 +++++++++++++++++++++++ 1 file changed, 272 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 1fd7ff51..039fa72b 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -1474,3 +1474,275 @@ Now we give the section of `arrow-map-equiv-iso-representable`. ( ψ)) ``` +We see that `arrow-map-equiv-iso-representable` has retraction +`arrow-inv-map-equiv-iso-representable`. + +```rzk +#def htpy-comp-map-equiv-inv-map-equiv + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( homotopy + ( hom A a' x) + ( hom A a' x) + ( comp + ( hom A a' x) + ( hom A a x) + ( hom A a' x) + ( map-equiv-iso-representable A is-segal-A a a' ψ x) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x)) + ( identity ( hom A a' x))) + := + \ x + → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) +``` +We compute the required paths for the retraction of +`arrow-map-iso-representable`. + +```rzk +#def compute-htpy-comp-map-equiv-inv-map-equiv -- p1 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : map-equiv-iso-representable A is-segal-A a a' ψ a' + ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( id-hom A a')) + = id-hom A a' + := htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ a' ( id-hom A a') + +#def eq-map-inv-map-equiv-iso-map--equiv-comp-arrow-map-idhom-a' -- p2 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : map-equiv-iso-representable A is-segal-A a a' ψ a' + ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( id-hom A a')) + = + map-equiv-iso-representable A is-segal-A a a' ψ a' + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a')) + := + ap + ( hom A a a') + ( hom A a' a') + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a' ( id-hom A a')) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a')) + ( map-equiv-iso-representable A is-segal-A a a' ψ a') + ( eq-compute-precomposition-evid + ( funext) + ( A) + ( is-segal-A) + ( a') + ( a) + ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( a') + ( id-hom A a')) + +#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map -- p3 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : map-equiv-iso-representable A is-segal-A a a' ψ a' + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a')) + = + map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + := + ap + ( hom A a a') + ( hom A a' a') + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a')) + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( map-equiv-iso-representable A is-segal-A a a' ψ a') + ( comp-id-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + +#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map2 -- p4 + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + = + comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a') + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + := + eq-compute-precomposition-evid + ( funext) + ( A) + ( is-segal-A) + ( a) + ( a') + ( map-equiv-iso-representable A is-segal-A a a' ψ) + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) +``` + +Concatenate all the paths above. + +```rzk +#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-m4 uses (funext) + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a') + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + = id-hom A a' + := + quadruple-concat + ( hom A a' a') + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a') + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a'))) + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( id-hom A a'))) + ( id-hom A a') + ( rev + ( hom A a' a') + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( comp-is-segal + ( A) + ( is-segal-A) + ( a') + ( a) + ( a') + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map2 + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( rev + ( hom A a' a') + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a'))) + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( rev + ( hom A a' a') + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( id-hom A a'))) + ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( comp-is-segal + ( A) + ( is-segal-A) + ( a) + ( a') + ( a') + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( id-hom A a'))) + ( eq-map-inv-map-equiv-iso-map--equiv-comp-arrow-map-idhom-a' + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ))) + ( compute-htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ) +``` + +Now we give the retraction of `arrow-map-equiv-iso-representable`. + +```rzk +#def retraction-arrow-map-equiv-iso-representable uses ( funext) + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : Retraction-arrow + ( A) + ( is-segal-A) + ( a') + ( a) + ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + := + ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ + , eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-m4 + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ)) +``` From da8633319356c6385c342126c82f9f7ae80d88c2 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 20 Nov 2023 13:39:09 -0500 Subject: [PATCH 08/20] change names and spacing --- src/simplicial-hott/10-rezk-types.rzk.md | 490 +++++++---------------- 1 file changed, 151 insertions(+), 339 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 039fa72b..e2e2ca6a 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -840,7 +840,15 @@ arrows. ## Representable isomorphisms. ```rzk -#def inverse-equiv-iso-representable +#def map-fiberwise-equiv + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : ( x : A) → ( hom A a x) → ( hom A a' x) + := \ x → first ( ψ x) + +#def inverse-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -852,31 +860,23 @@ arrows. ( first ( ψ x)) ( second ( ψ x))) -#def map-equiv-iso-representable - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : ( x : A) → ( hom A a x) → ( hom A a' x) - := \ x → first ( ψ x) - -#def inv-map-equiv-iso-representable +#def inv-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : ( x : A) → ( hom A a' x) → ( hom A a x) - := \ x → first ( ( inverse-equiv-iso-representable A is-segal-A a a' ψ) x) + := \ x → first ( ( inverse-fiberwise-equiv A is-segal-A a a' ψ) x) -#def arrow-map-equiv-iso-representable +#def arr-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : hom A a' a - := evid A a ( hom A a') ( map-equiv-iso-representable A is-segal-A a a' ψ) + := evid A a ( hom A a') ( map-fiberwise-equiv A is-segal-A a a' ψ) -#def arrow-inv-map-equiv-iso-representable +#def arr-inv-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -887,14 +887,14 @@ arrows. ( A) ( a') ( hom A a) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` We now show that `arrow-map-equiv-iso-representable` section `arrow-inv-map-equiv-iso-representable`. ```rzk -#def htpy-comp-inv-map-equiv-map-equiv +#def htpy-inv-map-fib-equiv-map-fib-equiv-id ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -906,45 +906,45 @@ We now show that `arrow-map-equiv-iso-representable` section ( hom A a x) ( hom A a' x) ( hom A a x) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x) - ( map-equiv-iso-representable A is-segal-A a a' ψ x)) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x) + ( map-fiberwise-equiv A is-segal-A a a' ψ x)) ( identity ( hom A a x))) := \ x - → first ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) + → first ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) ``` We compute the required paths for the section of `arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-inv-map-equiv-map-equiv +#def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-equiv-iso-representable A is-segal-A a a' ψ a - ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) ( id-hom A a)) + : inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) = id-hom A a - := htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ a ( id-hom A a) + := htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ a ( id-hom A a) -#def eq-inv-map-map-equiv-iso-inv-map-comp-arrow-map-idhom-a +#def ap-inv-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-equiv-iso-representable A is-segal-A a a' ψ a - ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + : inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) = - inv-map-equiv-iso-representable A is-segal-A a a' ψ a + inv-map-fiberwise-equiv A is-segal-A a a' ψ a ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable + ( arr-map-fiberwise-equiv ( A) ( is-segal-A) ( a) @@ -955,49 +955,39 @@ We compute the required paths for the section of ap ( hom A a' a) ( hom A a a) - ( map-equiv-iso-representable A is-segal-A a a' ψ a ( id-hom A a)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a)) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a) ( eq-compute-precomposition-evid ( funext) ( A) ( is-segal-A) ( a) ( a') - ( map-equiv-iso-representable A is-segal-A a a' ψ) + ( map-fiberwise-equiv A is-segal-A a a' ψ) ( a) ( id-hom A a)) -#def eq-inv-map-comp-arr-map-equiv-comp-arrow-inv-map-equiv-comp-arr-map-equiv +#def eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-equiv-iso-representable A is-segal-A a a' ψ a + : inv-map-fiberwise-equiv A is-segal-A a a' ψ a ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) = comp-is-segal @@ -1006,24 +996,14 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) := eq-compute-precomposition-evid @@ -1032,7 +1012,7 @@ We compute the required paths for the section of ( is-segal-A) ( a') ( a) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( a) ( comp-is-segal ( A) @@ -1040,15 +1020,10 @@ We compute the required paths for the section of ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) -#def eq-comp-comp-arrow-inv-map-arr-map-comp-arr-inv-map-comp-arr-map-idhom-a +#def associative-is-segal-comp-comp-arr-inv-equi-arr-map-idhom-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1065,18 +1040,8 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( id-hom A a) = comp-is-segal @@ -1085,24 +1050,14 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) := associative-is-segal @@ -1113,21 +1068,11 @@ We compute the required paths for the section of ( a') ( a) ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a) -#def eq-comp-comp-inv-map-equiv-arr-map-idhom-a-comp-arr-inv-map-arr-map +#def comp-id-comp-arr-inv-map-arr-map-id-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1144,18 +1089,8 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( id-hom A a) = ( comp-is-segal @@ -1164,18 +1099,8 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) := comp-id-is-segal ( A) @@ -1188,24 +1113,14 @@ We compute the required paths for the section of ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ``` Concatenate all the paths above. ```rzk -#def eq-comp-arrow-inv-map-arrow-map-equiv-iso-representable uses (extext funext) +#def eq-comp-arrow-inv-map-arrow-map-equiv-id-a uses (extext funext) ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1216,18 +1131,8 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) = id-hom A a := quintuple-concat @@ -1238,18 +1143,8 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( comp-is-segal ( A) ( is-segal-A) @@ -1262,18 +1157,8 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( id-hom A a)) ( comp-is-segal ( A) @@ -1281,41 +1166,26 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a))) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a))) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a - ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a))) ( id-hom A a) ( rev @@ -1332,18 +1202,8 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( id-hom A a)) ( comp-is-segal ( A) @@ -1351,25 +1211,10 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( eq-comp-comp-inv-map-equiv-arr-map-idhom-a-comp-arr-inv-map-arr-map - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( eq-comp-comp-arrow-inv-map-arr-map-comp-arr-inv-map-comp-arr-map-idhom-a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( comp-id-comp-arr-inv-map-arr-map-id-a A is-segal-A a a' ψ)) + ( associative-is-segal-comp-comp-arr-inv-equi-arr-map-idhom-a ( A) ( is-segal-A) ( a) @@ -1377,19 +1222,14 @@ Concatenate all the paths above. ( ψ)) ( rev ( hom A a a) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a))) ( comp-is-segal ( A) @@ -1397,26 +1237,16 @@ Concatenate all the paths above. ( a) ( a') ( a) - ( arrow-inv-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a)) ) - ( eq-inv-map-comp-arr-map-equiv-comp-arrow-inv-map-equiv-comp-arr-map-equiv + ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv ( A) ( is-segal-A) ( a) @@ -1424,30 +1254,20 @@ Concatenate all the paths above. ( ψ))) ( rev ( hom A a a) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a - ( ( map-equiv-iso-representable A is-segal-A a a' ψ a) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a))) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a) - ( arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a))) - ( eq-inv-map-map-equiv-iso-inv-map-comp-arrow-map-idhom-a - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( compute-htpy-comp-inv-map-equiv-map-equiv A is-segal-A a a' ψ) + ( ap-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) ``` Now we give the section of `arrow-map-equiv-iso-representable`. @@ -1463,22 +1283,17 @@ Now we give the section of `arrow-map-equiv-iso-representable`. ( is-segal-A) ( a') ( a) - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ - , eq-comp-arrow-inv-map-arrow-map-equiv-iso-representable - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ + , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) ``` We see that `arrow-map-equiv-iso-representable` has retraction `arrow-inv-map-equiv-iso-representable`. ```rzk -#def htpy-comp-map-equiv-inv-map-equiv +#def htpy-comp-map-fib-equiv-inv-map-fib-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1490,87 +1305,87 @@ We see that `arrow-map-equiv-iso-representable` has retraction ( hom A a' x) ( hom A a x) ( hom A a' x) - ( map-equiv-iso-representable A is-segal-A a a' ψ x) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ x)) + ( map-fiberwise-equiv A is-segal-A a a' ψ x) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x)) ( identity ( hom A a' x))) := \ x - → second ( second ( inverse-equiv-iso-representable A is-segal-A a a' ψ x)) + → second ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) ``` We compute the required paths for the retraction of `arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-map-equiv-inv-map-equiv -- p1 +#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv -- p1 ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-equiv-iso-representable A is-segal-A a a' ψ a' - ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + : map-fiberwise-equiv A is-segal-A a a' ψ a' + ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') ( id-hom A a')) = id-hom A a' - := htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ a' ( id-hom A a') + := htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ a' ( id-hom A a') -#def eq-map-inv-map-equiv-iso-map--equiv-comp-arrow-map-idhom-a' -- p2 +#def ap-map-fiberwise-equiv -- p2 ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-equiv-iso-representable A is-segal-A a a' ψ a' - ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + : map-fiberwise-equiv A is-segal-A a a' ψ a' + ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') ( id-hom A a')) = - map-equiv-iso-representable A is-segal-A a a' ψ a' + map-fiberwise-equiv A is-segal-A a a' ψ a' ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a')) := ap ( hom A a a') ( hom A a' a') - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a' ( id-hom A a')) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a')) - ( map-equiv-iso-representable A is-segal-A a a' ψ a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a') ( eq-compute-precomposition-evid ( funext) ( A) ( is-segal-A) ( a') ( a) - ( inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( a') ( id-hom A a')) -#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map -- p3 +#def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map -- p3 ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-equiv-iso-representable A is-segal-A a a' ψ a' + : map-fiberwise-equiv A is-segal-A a a' ψ a' ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a')) = - map-equiv-iso-representable A is-segal-A a a' ψ a' - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) := ap ( hom A a a') @@ -1581,24 +1396,24 @@ We compute the required paths for the retraction of ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a')) - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) - ( map-equiv-iso-representable A is-segal-A a a' ψ a') + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( map-fiberwise-equiv A is-segal-A a a' ψ a') ( comp-id-is-segal ( A) ( is-segal-A) ( a) ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) -#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map2 -- p4 +#def eq-compute-precomposition-evid-map-fiberwise-equiv -- p4 ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-equiv-iso-representable A is-segal-A a a' ψ a' - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + : map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) = comp-is-segal ( A) @@ -1606,8 +1421,8 @@ We compute the required paths for the retraction of ( a') ( a) ( a') - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) := eq-compute-precomposition-evid ( funext) @@ -1615,15 +1430,15 @@ We compute the required paths for the retraction of ( is-segal-A) ( a) ( a') - ( map-equiv-iso-representable A is-segal-A a a' ψ) + ( map-fiberwise-equiv A is-segal-A a a' ψ) ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` Concatenate all the paths above. ```rzk -#def eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-m4 uses (funext) +#def eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' uses (funext) ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1634,8 +1449,8 @@ Concatenate all the paths above. ( a') ( a) ( a') - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) = id-hom A a' := quadruple-concat @@ -1646,36 +1461,36 @@ Concatenate all the paths above. ( a') ( a) ( a') - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) - ( map-equiv-iso-representable A is-segal-A a a' ψ a' - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) - ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a'))) - ( map-equiv-iso-representable A is-segal-A a a' ψ a' - ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') ( id-hom A a'))) ( id-hom A a') ( rev ( hom A a' a') - ( map-equiv-iso-representable A is-segal-A a a' ψ a' - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) ( comp-is-segal ( A) ( is-segal-A) ( a') ( a) ( a') - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) - ( eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map2 + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( eq-compute-precomposition-evid-map-fiberwise-equiv ( A) ( is-segal-A) ( a) @@ -1683,18 +1498,18 @@ Concatenate all the paths above. ( ψ))) ( rev ( hom A a' a') - ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( map-fiberwise-equiv A is-segal-A a a' ψ a' ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a'))) - ( map-equiv-iso-representable A is-segal-A a a' ψ a' - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ)) - ( eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-map + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map ( A) ( is-segal-A) ( a) @@ -1702,25 +1517,20 @@ Concatenate all the paths above. ( ψ))) ( rev ( hom A a' a') - ( map-equiv-iso-representable A is-segal-A a a' ψ a' - ( ( inv-map-equiv-iso-representable A is-segal-A a a' ψ a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') ( id-hom A a'))) - ( map-equiv-iso-representable A is-segal-A a a' ψ a' + ( map-fiberwise-equiv A is-segal-A a a' ψ a' ( comp-is-segal ( A) ( is-segal-A) ( a) ( a') ( a') - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( id-hom A a'))) - ( eq-map-inv-map-equiv-iso-map--equiv-comp-arrow-map-idhom-a' - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( compute-htpy-comp-map-equiv-inv-map-equiv A is-segal-A a a' ψ) + ( ap-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) ``` Now we give the retraction of `arrow-map-equiv-iso-representable`. @@ -1736,13 +1546,15 @@ Now we give the retraction of `arrow-map-equiv-iso-representable`. ( is-segal-A) ( a') ( a) - ( arrow-map-equiv-iso-representable A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - ( arrow-inv-map-equiv-iso-representable A is-segal-A a a' ψ - , eq-map-equiv-iso-comp-arr-inv-map-map-equiv-iso-arrow-inv-m4 + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ + , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' ( A) ( is-segal-A) ( a) ( a') ( ψ)) ``` + +We show that representable arrows are isomophisms. From afbb24d0c4535c3964efafbcb3f29809bfa84d54 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 20 Nov 2023 14:20:13 -0500 Subject: [PATCH 09/20] proof of prop 10.11 --- src/simplicial-hott/10-rezk-types.rzk.md | 69 ++++++++++++++++++------ 1 file changed, 54 insertions(+), 15 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index e2e2ca6a..92d66c67 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -890,8 +890,8 @@ arrows. ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` -We now show that `arrow-map-equiv-iso-representable` section -`arrow-inv-map-equiv-iso-representable`. +We now show that `arrow-map-fiberwise-equiv` has section +`arrow-inv-map-fiberwise-equiv`. ```rzk #def htpy-inv-map-fib-equiv-map-fib-equiv-id @@ -915,7 +915,7 @@ We now show that `arrow-map-equiv-iso-representable` section ``` We compute the required paths for the section of -`arrow-map-iso-representable`. +`arrow-map-fiberwise-equiv`. ```rzk #def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id @@ -1270,10 +1270,10 @@ Concatenate all the paths above. ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) ``` -Now we give the section of `arrow-map-equiv-iso-representable`. +Now we give the section of `arrow-map-fiberwise-equiv`. ```rzk -#def section-arrow-map-iso-representable uses ( extext funext) +#def section-arrow-map-fiberwise-equiv uses ( extext funext) ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1289,8 +1289,8 @@ Now we give the section of `arrow-map-equiv-iso-representable`. , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) ``` -We see that `arrow-map-equiv-iso-representable` has retraction -`arrow-inv-map-equiv-iso-representable`. +We see that `arrow-map-fiberwise-equiv` has retraction +`arrow-inv-map-fiberwise-equiv`. ```rzk #def htpy-comp-map-fib-equiv-inv-map-fib-equiv @@ -1316,7 +1316,7 @@ We compute the required paths for the retraction of `arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv -- p1 +#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1325,9 +1325,16 @@ We compute the required paths for the retraction of ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') ( id-hom A a')) = id-hom A a' - := htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ a' ( id-hom A a') + := htpy-comp-map-fib-equiv-inv-map-fib-equiv + ( A) + ( is-segal-A) + ( a) + ( a') + ( ψ) + ( a') + ( id-hom A a') -#def ap-map-fiberwise-equiv -- p2 +#def ap-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1369,7 +1376,7 @@ We compute the required paths for the retraction of ( a') ( id-hom A a')) -#def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map -- p3 +#def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1407,7 +1414,7 @@ We compute the required paths for the retraction of ( a') ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) -#def eq-compute-precomposition-evid-map-fiberwise-equiv -- p4 +#def eq-compute-precomposition-evid-map-fiberwise-equiv ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1533,10 +1540,10 @@ Concatenate all the paths above. ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) ``` -Now we give the retraction of `arrow-map-equiv-iso-representable`. +Now we give the retraction of `arrow-map-fiberwise-equiv`. ```rzk -#def retraction-arrow-map-equiv-iso-representable uses ( funext) +#def retraction-arrow-map-fiberwise-equiv uses ( funext) ( A : U) ( is-segal-A : is-segal A) ( a a' : A) @@ -1557,4 +1564,36 @@ Now we give the retraction of `arrow-map-equiv-iso-representable`. ( ψ)) ``` -We show that representable arrows are isomophisms. +We show that arrows from fiberwise equivalences are isomorphisms. + +```rzk tittle="RS17, Proposition 10.11 (i)" +#def representable-isomorphism uses ( extext funext) + ( A : U) + ( is-segal-A : is-segal A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : is-iso-arrow + ( A) + ( is-segal-A) + ( a') + ( a) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + := + ( retraction-arrow-map-fiberwise-equiv A is-segal-A a a' ψ + , section-arrow-map-fiberwise-equiv A is-segal-A a a' ψ) + +#def eq-representable-isomorphism uses ( extext funext) + ( A : U) + ( is-rezk-A : is-rezk A) + ( a a' : A) + ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + : a' = a + := + eq-iso-is-rezk + ( A) + ( is-rezk-A) + ( a') + ( a) + ( arr-map-fiberwise-equiv A ( first is-rezk-A) a a' ψ + , representable-isomorphism A ( first is-rezk-A) a a' ψ) +``` From 3ed280ff450fdbe37dd89f429f9d834aa93b2184 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 20 Nov 2023 14:42:03 -0500 Subject: [PATCH 10/20] last eddits and format --- src/simplicial-hott/10-rezk-types.rzk.md | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 92d66c67..5085c170 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -890,8 +890,8 @@ arrows. ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` -We now show that `arrow-map-fiberwise-equiv` has section -`arrow-inv-map-fiberwise-equiv`. +We now show that `#!rzk arrow-map-fiberwise-equiv` has section +`#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk #def htpy-inv-map-fib-equiv-map-fib-equiv-id @@ -915,7 +915,7 @@ We now show that `arrow-map-fiberwise-equiv` has section ``` We compute the required paths for the section of -`arrow-map-fiberwise-equiv`. +`#!rzk arrow-map-fiberwise-equiv`. ```rzk #def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id @@ -1270,7 +1270,7 @@ Concatenate all the paths above. ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) ``` -Now we give the section of `arrow-map-fiberwise-equiv`. +Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. ```rzk #def section-arrow-map-fiberwise-equiv uses ( extext funext) @@ -1289,8 +1289,8 @@ Now we give the section of `arrow-map-fiberwise-equiv`. , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) ``` -We see that `arrow-map-fiberwise-equiv` has retraction -`arrow-inv-map-fiberwise-equiv`. +We see that `#!rzk arrow-map-fiberwise-equiv` has retraction +`#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk #def htpy-comp-map-fib-equiv-inv-map-fib-equiv @@ -1312,8 +1312,9 @@ We see that `arrow-map-fiberwise-equiv` has retraction \ x → second ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) ``` + We compute the required paths for the retraction of -`arrow-map-iso-representable`. +`#!rzk arrow-map-iso-representable`. ```rzk #def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv @@ -1540,7 +1541,7 @@ Concatenate all the paths above. ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) ``` -Now we give the retraction of `arrow-map-fiberwise-equiv`. +Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. ```rzk #def retraction-arrow-map-fiberwise-equiv uses ( funext) @@ -1566,7 +1567,7 @@ Now we give the retraction of `arrow-map-fiberwise-equiv`. We show that arrows from fiberwise equivalences are isomorphisms. -```rzk tittle="RS17, Proposition 10.11 (i)" +```rzk title="RS17, Proposition 10.11 (i)" #def representable-isomorphism uses ( extext funext) ( A : U) ( is-segal-A : is-segal A) @@ -1581,7 +1582,11 @@ We show that arrows from fiberwise equivalences are isomorphisms. := ( retraction-arrow-map-fiberwise-equiv A is-segal-A a a' ψ , section-arrow-map-fiberwise-equiv A is-segal-A a a' ψ) +``` + +The second part of Proposition 10.11. +```rzk title="RS17, Proposition 10.11 (ii)" #def eq-representable-isomorphism uses ( extext funext) ( A : U) ( is-rezk-A : is-rezk A) From 3238405313e2d71bdb896beb8de3bd45cf0fcc90 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 20 Nov 2023 15:49:18 -0500 Subject: [PATCH 11/20] formating --- src/simplicial-hott/10-rezk-types.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index b4dc022f..d709f2f9 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -944,8 +944,8 @@ In particular, every contractible type is Rezk ## Representable isomorphisms. -We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise equivalence -with no extra data, and then define some helpers. +We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise +equivalence with no extra data, and then define some helpers. ```rzk #def map-fiberwise-equiv From 443e3f8bdc21f20d7982cfbfc7f9d75bb0d73340 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Thu, 23 Nov 2023 10:19:26 -0500 Subject: [PATCH 12/20] indentation --- src/simplicial-hott/10-rezk-types.rzk.md | 805 ++++++++--------------- 1 file changed, 263 insertions(+), 542 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index d709f2f9..e95ee24a 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -962,11 +962,13 @@ equivalence with no extra data, and then define some helpers. ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : ( x : A) → ( has-inverse ( hom A a x) ( hom A a' x) ( first ( ψ x))) - := \ x → ( has-inverse-is-equiv - ( hom A a x) - ( hom A a' x) - ( first ( ψ x)) - ( second ( ψ x))) + := + \ x → + has-inverse-is-equiv + ( hom A a x) + ( hom A a' x) + ( first ( ψ x)) + ( second ( ψ x)) #def inv-map-fiberwise-equiv ( A : U) @@ -974,7 +976,7 @@ equivalence with no extra data, and then define some helpers. ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : ( x : A) → ( hom A a' x) → ( hom A a x) - := \ x → first ( ( inverse-fiberwise-equiv A is-segal-A a a' ψ) x) + := \ x → first ( inverse-fiberwise-equiv A is-segal-A a a' ψ x) #def arr-map-fiberwise-equiv ( A : U) @@ -990,12 +992,7 @@ equivalence with no extra data, and then define some helpers. ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : hom A a a' - := - evid - ( A) - ( a') - ( hom A a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + := evid A a' ( hom A a) ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` We now show that `#!rzk arrow-map-fiberwise-equiv` has section @@ -1007,19 +1004,18 @@ We now show that `#!rzk arrow-map-fiberwise-equiv` has section ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : ( x : A) → ( homotopy - ( hom A a x) - ( hom A a x) - ( comp - ( hom A a x) - ( hom A a' x) - ( hom A a x) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x) - ( map-fiberwise-equiv A is-segal-A a a' ψ x)) - ( identity ( hom A a x))) - := - \ x - → first ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) + : ( x : A) + → ( homotopy + ( hom A a x) + ( hom A a x) + ( comp + ( hom A a x) + ( hom A a' x) + ( hom A a x) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x) + ( map-fiberwise-equiv A is-segal-A a a' ψ x)) + ( identity ( hom A a x))) + := \ x → first ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) ``` We compute the required paths for the section of @@ -1032,8 +1028,9 @@ We compute the required paths for the section of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) - = id-hom A a + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) + =_{ hom A a a} + id-hom A a := htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ a ( id-hom A a) #def ap-inv-map-fiberwise-equiv @@ -1042,46 +1039,25 @@ We compute the required paths for the section of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) - ( id-hom A a)) - = + ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) + =_{ hom A a a} inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( id-hom A a)) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) := - ap - ( hom A a' a) - ( hom A a a) - ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a)) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a) - ( eq-compute-precomposition-evid - ( funext) - ( A) - ( is-segal-A) - ( a) - ( a') - ( map-fiberwise-equiv A is-segal-A a a' ψ) - ( a) - ( id-hom A a)) + ap + ( hom A a' a) + ( hom A a a) + ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a)) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a) + ( eq-compute-precomposition-evid funext A is-segal-A a a' + ( map-fiberwise-equiv A is-segal-A a a' ψ) + ( a) + ( id-hom A a)) #def eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv ( A : U) @@ -1089,140 +1065,64 @@ We compute the required paths for the section of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) - = - comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) + =_{ hom A a a} + comp-is-segal A is-segal-A a a' a ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) := - eq-compute-precomposition-evid - ( funext) - ( A) - ( is-segal-A) - ( a') - ( a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) - -#def associative-is-segal-comp-comp-arr-inv-equi-arr-map-idhom-a + eq-compute-precomposition-evid funext A is-segal-A a' a + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( a) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) + +#def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + : comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ( id-hom A a) - = - comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) + =_{ hom A a a} + comp-is-segal A is-segal-A a a' a ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) - := - associative-is-segal - ( extext) - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( comp-is-segal A is-segal-A a' a a ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a) + ( id-hom A a)) + := + associative-is-segal extext A is-segal-A a a' a a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a) #def comp-id-comp-arr-inv-map-arr-map-id-a ( A : U) ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( id-hom A a) - = - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) + : comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( id-hom A a) + =_{ hom A a a} + comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - comp-id-is-segal - ( A) - ( is-segal-A) - ( a) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + comp-id-is-segal A is-segal-A a a + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) ``` Concatenate all the paths above. @@ -1233,149 +1133,73 @@ Concatenate all the paths above. ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : comp-is-segal + : comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + =_{ hom A a a} + id-hom A a + := + quintuple-concat + ( hom A a a) + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( id-hom A a)) + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a))) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a))) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a))) + ( id-hom A a) + ( rev + ( hom A a a) + ( comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( id-hom A a)) + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( comp-id-comp-arr-inv-map-arr-map-id-a A is-segal-A a a' ψ)) + ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a A is-segal-A a a' ψ) + ( rev + ( hom A a a) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a))) + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a)) ) + ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv ( A) ( is-segal-A) ( a) ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - = id-hom A a - := - quintuple-concat - ( hom A a a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( id-hom A a)) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) - ( id-hom A a))) - ( id-hom A a) - ( rev - ( hom A a a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a) - ( a) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( id-hom A a)) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( comp-id-comp-arr-inv-map-arr-map-id-a A is-segal-A a a' ψ)) - ( associative-is-segal-comp-comp-arr-inv-equi-arr-map-idhom-a - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) - ( rev - ( hom A a a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) ) - ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( rev - ( hom A a a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) - ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( ap-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) + ( ψ))) + ( rev + ( hom A a a) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a))) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a + ( comp-is-segal A is-segal-A a' a a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a))) + ( ap-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) ``` Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. @@ -1386,15 +1210,11 @@ Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : Section-arrow - ( A) - ( is-segal-A) - ( a') - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + : Section-arrow A is-segal-A a' a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ - , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ + , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) ``` We see that `#!rzk arrow-map-fiberwise-equiv` has retraction @@ -1406,19 +1226,18 @@ We see that `#!rzk arrow-map-fiberwise-equiv` has retraction ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : ( x : A) → ( homotopy - ( hom A a' x) - ( hom A a' x) - ( comp - ( hom A a' x) - ( hom A a x) - ( hom A a' x) - ( map-fiberwise-equiv A is-segal-A a a' ψ x) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x)) - ( identity ( hom A a' x))) - := - \ x - → second ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) + : ( x : A) + → ( homotopy + ( hom A a' x) + ( hom A a' x) + ( comp + ( hom A a' x) + ( hom A a x) + ( hom A a' x) + ( map-fiberwise-equiv A is-segal-A a a' ψ x) + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x)) + ( identity ( hom A a' x))) + := \ x → second ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) ``` We compute the required paths for the retraction of @@ -1431,17 +1250,11 @@ We compute the required paths for the retraction of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') - ( id-hom A a')) - = id-hom A a' - := htpy-comp-map-fib-equiv-inv-map-fib-equiv - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ) - ( a') - ( id-hom A a') + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) + =_{ hom A a' a'} + id-hom A a' + := + htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ a' ( id-hom A a') #def ap-map-fiberwise-equiv ( A : U) @@ -1449,41 +1262,25 @@ We compute the required paths for the retraction of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') - ( id-hom A a')) - = + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) + =_{ hom A a' a'} map-fiberwise-equiv A is-segal-A a a' ψ a' - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a')) + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a')) := - ap - ( hom A a a') - ( hom A a' a') - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a')) - ( map-fiberwise-equiv A is-segal-A a a' ψ a') - ( eq-compute-precomposition-evid - ( funext) - ( A) - ( is-segal-A) - ( a') - ( a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( a') - ( id-hom A a')) + ap + ( hom A a a') + ( hom A a' a') + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a')) + ( map-fiberwise-equiv A is-segal-A a a' ψ a') + ( eq-compute-precomposition-evid funext A is-segal-A a' a + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( a') + ( id-hom A a')) #def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map ( A : U) @@ -1491,37 +1288,23 @@ We compute the required paths for the retraction of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a')) - = - map-fiberwise-equiv A is-segal-A a a' ψ a' + ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a')) + =_{ hom A a' a'} + map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) := - ap - ( hom A a a') - ( hom A a' a') - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a')) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( map-fiberwise-equiv A is-segal-A a a' ψ a') - ( comp-id-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ap + ( hom A a a') + ( hom A a' a') + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a')) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( map-fiberwise-equiv A is-segal-A a a' ψ a') + ( comp-id-is-segal A is-segal-A a a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) #def eq-compute-precomposition-evid-map-fiberwise-equiv ( A : U) @@ -1529,26 +1312,16 @@ We compute the required paths for the retraction of ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - = - comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a') + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + =_{ hom A a' a'} + comp-is-segal A is-segal-A a' a a' ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) := - eq-compute-precomposition-evid - ( funext) - ( A) - ( is-segal-A) - ( a) - ( a') - ( map-fiberwise-equiv A is-segal-A a a' ψ) - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + eq-compute-precomposition-evid funext A is-segal-A a a' + ( map-fiberwise-equiv A is-segal-A a a' ψ) + ( a') + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) ``` Concatenate all the paths above. @@ -1559,94 +1332,59 @@ Concatenate all the paths above. ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : comp-is-segal + : comp-is-segal A is-segal-A a' a a' + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + =_{ hom A a' a'} + id-hom A a' + := + quadruple-concat + ( hom A a' a') + ( comp-is-segal A is-segal-A a' a a' + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a'))) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') + ( id-hom A a'))) + ( id-hom A a') + ( rev + ( hom A a' a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( comp-is-segal A is-segal-A a' a a' + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( eq-compute-precomposition-evid-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( rev + ( hom A a' a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a'))) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map ( A) ( is-segal-A) - ( a') ( a) ( a') - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - = id-hom A a' - := - quadruple-concat - ( hom A a' a') - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a') - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') - ( id-hom A a'))) - ( id-hom A a') - ( rev - ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( comp-is-segal - ( A) - ( is-segal-A) - ( a') - ( a) - ( a') - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( eq-compute-precomposition-evid-map-fiberwise-equiv - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( rev - ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) - ( rev - ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') - ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( comp-is-segal - ( A) - ( is-segal-A) - ( a) - ( a') - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a'))) - ( ap-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) + ( ψ))) + ( rev + ( hom A a' a') + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a'))) + ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( id-hom A a'))) + ( ap-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) ``` Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. @@ -1657,20 +1395,11 @@ Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : Retraction-arrow - ( A) - ( is-segal-A) - ( a') - ( a) + : Retraction-arrow A is-segal-A a' a ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ - , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ)) + ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ + , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' A is-segal-A a a' ψ) ``` We show that arrows from fiberwise equivalences are isomorphisms. @@ -1681,15 +1410,11 @@ We show that arrows from fiberwise equivalences are isomorphisms. ( is-segal-A : is-segal A) ( a a' : A) ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : is-iso-arrow - ( A) - ( is-segal-A) - ( a') - ( a) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + : is-iso-arrow A is-segal-A a' a + ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) := - ( retraction-arrow-map-fiberwise-equiv A is-segal-A a a' ψ - , section-arrow-map-fiberwise-equiv A is-segal-A a a' ψ) + ( retraction-arrow-map-fiberwise-equiv A is-segal-A a a' ψ + , section-arrow-map-fiberwise-equiv A is-segal-A a a' ψ) ``` The second part of Proposition 10.11. @@ -1702,11 +1427,7 @@ The second part of Proposition 10.11. ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : a' = a := - eq-iso-is-rezk - ( A) - ( is-rezk-A) - ( a') - ( a) - ( arr-map-fiberwise-equiv A ( first is-rezk-A) a a' ψ - , representable-isomorphism A ( first is-rezk-A) a a' ψ) + eq-iso-is-rezk A is-rezk-A a' a + ( arr-map-fiberwise-equiv A ( first is-rezk-A) a a' ψ + , representable-isomorphism A ( first is-rezk-A) a a' ψ) ``` From cd438ab5b7ce99def3e276fc57138feae7be1c64 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Thu, 23 Nov 2023 14:45:01 -0500 Subject: [PATCH 13/20] typo fixed --- src/simplicial-hott/07-discrete.rzk.md | 52 +++++++++++++++++++++----- 1 file changed, 43 insertions(+), 9 deletions(-) diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index 2b419242..1c5bc443 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -13,9 +13,9 @@ This is a literate `rzk` file: - `hott/01-paths.rzk.md` - We require basic path algebra. - `hott/04-equivalences.rzk.md` - We require the notion of equivalence between types. -- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and +- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and their subshapes. -- `04-extension-types.rzk.md` — We use extension extensionality. +- `03-extension-types.rzk.md` — We use extension extensionality. - `05-segal-types.rzk.md` - We use the notion of hom types. Some of the definitions in this file rely on function extensionality and @@ -252,8 +252,7 @@ of discrete types is discrete. ``` By extension extensionality, an extension type into a family of discrete types -is discrete. Since `#!rzk equiv-extensions-BOT-equiv` considers total extension -types only, extending from `#!rzk BOT`, that's all we prove here for now. +is discrete. ```rzk #def equiv-hom-eq-extension-type-is-discrete uses (extext) @@ -270,13 +269,11 @@ types only, extending from `#!rzk BOT`, that's all we prove here for now. ( (t : ψ) → hom (A t) (f t) (g t)) ( hom ((t : ψ) → A t) f g) ( equiv-ExtExt extext I ψ (\ _ → BOT) A (\ _ → recBOT) f g) - ( equiv-extensions-BOT-equiv - ( extext) - ( I) - ( ψ) + ( equiv-extensions-equiv extext I ψ (\ _ → BOT) ( \ t → f t = g t) ( \ t → hom (A t) (f t) (g t)) - ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t))))) + ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t)))) + ( \ _ → recBOT)) ( fubini ( I) ( 2) @@ -1141,3 +1138,40 @@ Finally, we conclude: : is-segal A := is-contr-hom2-is-discrete A is-discrete-A ``` + +## Naturality for hom-eq + +`#!rzk hom-eq` commute with `#!rzk ap-hom`. + +```rzk +#def hom-eq-naturality + ( A B : U) + ( f : A → B) + ( x y : A) + ( p : x = y) + : + comp (x = y) (hom A x y) (hom B (f x) (f y)) + ( ap-hom A B f x y) + ( hom-eq A x y) + ( p) + = + comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) + ( hom-eq B (f x) (f y)) + ( ap A B x y f) + ( p) + := + ind-path A x + ( \ y' p' → + comp (x = y') (hom A x y') (hom B (f x) (f y')) + ( ap-hom A B f x y') + ( hom-eq A x y') + ( p') + = + comp (x = y') ((f x) = (f y')) (hom B (f x) (f y')) + ( hom-eq B (f x) (f y')) + ( ap A B x y' f) + ( p')) + ( functors-pres-id extext A B f x) + ( y) + ( p) +``` From 8c97aa7ee4113e66506286ea8f9b52d8fa222b6f Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Thu, 30 Nov 2023 12:27:18 -0500 Subject: [PATCH 14/20] streamline by adding section --- src/simplicial-hott/10-rezk-types.rzk.md | 397 ++++++++--------------- 1 file changed, 144 insertions(+), 253 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index e95ee24a..681352c0 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -948,19 +948,18 @@ We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise equivalence with no extra data, and then define some helpers. ```rzk +#section representable-isomorphisms + +#variable A : U +#variable is-segal-A : is-segal A +#variables a a' : A +#variable ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x)) + #def map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : ( x : A) → ( hom A a x) → ( hom A a' x) := \ x → first ( ψ x) #def inverse-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : ( x : A) → ( has-inverse ( hom A a x) ( hom A a' x) ( first ( ψ x))) := \ x → @@ -970,40 +969,24 @@ equivalence with no extra data, and then define some helpers. ( first ( ψ x)) ( second ( ψ x)) -#def inv-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def inv-map-fiberwise-equiv uses ( A a a' ψ) : ( x : A) → ( hom A a' x) → ( hom A a x) - := \ x → first ( inverse-fiberwise-equiv A is-segal-A a a' ψ x) + := \ x → first ( inverse-fiberwise-equiv x) #def arr-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : hom A a' a - := evid A a ( hom A a') ( map-fiberwise-equiv A is-segal-A a a' ψ) + := evid A a ( hom A a') ( map-fiberwise-equiv ) #def arr-inv-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) : hom A a a' - := evid A a' ( hom A a) ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + := evid A a' ( hom A a) ( inv-map-fiberwise-equiv) ``` We now show that `#!rzk arrow-map-fiberwise-equiv` has section `#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk -#def htpy-inv-map-fib-equiv-map-fib-equiv-id - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def htpy-inv-map-fib-equiv-map-fib-equiv-id uses ( A a a' ψ) : ( x : A) → ( homotopy ( hom A a x) @@ -1012,10 +995,10 @@ We now show that `#!rzk arrow-map-fiberwise-equiv` has section ( hom A a x) ( hom A a' x) ( hom A a x) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x) - ( map-fiberwise-equiv A is-segal-A a a' ψ x)) + ( inv-map-fiberwise-equiv x) + ( map-fiberwise-equiv x)) ( identity ( hom A a x))) - := \ x → first ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) + := \ x → first ( second ( inverse-fiberwise-equiv x)) ``` We compute the required paths for the section of @@ -1023,209 +1006,158 @@ We compute the required paths for the section of ```rzk #def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) + : inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a)) =_{ hom A a a} id-hom A a - := htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ a ( id-hom A a) + := htpy-inv-map-fib-equiv-map-fib-equiv-id a ( id-hom A a) -#def ap-inv-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( ( map-fiberwise-equiv A is-segal-A a a' ψ a) ( id-hom A a)) +#def ap-inv-map-fiberwise-equiv uses ( A is-segal-A a a' ψ) + : inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a)) =_{ hom A a a} - inv-map-fiberwise-equiv A is-segal-A a a' ψ a + inv-map-fiberwise-equiv a ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) := ap ( hom A a' a) ( hom A a a) - ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a)) + ( map-fiberwise-equiv a ( id-hom A a)) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a) + ( inv-map-fiberwise-equiv a) ( eq-compute-precomposition-evid funext A is-segal-A a a' - ( map-fiberwise-equiv A is-segal-A a a' ψ) + ( map-fiberwise-equiv) ( a) ( id-hom A a)) #def eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : inv-map-fiberwise-equiv A is-segal-A a a' ψ a + uses ( A is-segal-A a a' ψ) + : inv-map-fiberwise-equiv a ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) := eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv) ( a) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) #def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + uses ( A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ( id-hom A a) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) ( id-hom A a)) := associative-is-segal extext A is-segal-A a a' a a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) + ( arr-map-fiberwise-equiv) ( id-hom A a) -#def comp-id-comp-arr-inv-map-arr-map-id-a - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def comp-id-comp-arr-inv-map-arr-map-id-a uses ( A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ( id-hom A a) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv := comp-id-is-segal A is-segal-A a a ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ``` Concatenate all the paths above. ```rzk -#def eq-comp-arrow-inv-map-arrow-map-equiv-id-a uses (extext funext) - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def eq-comp-arrow-inv-map-arrow-map-equiv-id-a + uses ( extext funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv =_{ hom A a a} id-hom A a := quintuple-concat ( hom A a a) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ( comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ( id-hom A a)) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a))) + ( arr-inv-map-fiberwise-equiv) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( inv-map-fiberwise-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a))) ( id-hom A a) ( rev ( hom A a a) ( comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) ( id-hom A a)) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( comp-id-comp-arr-inv-map-arr-map-id-a A is-segal-A a a' ψ)) - ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a A is-segal-A a a' ψ) + arr-inv-map-fiberwise-equiv + arr-map-fiberwise-equiv) + ( comp-id-comp-arr-inv-map-arr-map-id-a)) + ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a) ( rev ( hom A a a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) + ( inv-map-fiberwise-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a)) ) - ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( arr-inv-map-fiberwise-equiv) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv)) ( rev ( hom A a a) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( map-fiberwise-equiv A is-segal-A a a' ψ a ( id-hom A a))) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a - ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a))) - ( ap-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a))) + ( inv-map-fiberwise-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( ap-inv-map-fiberwise-equiv)) + ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id) ``` Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. ```rzk -#def section-arrow-map-fiberwise-equiv uses ( extext funext) - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : Section-arrow A is-segal-A a' a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - := - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ - , eq-comp-arrow-inv-map-arrow-map-equiv-id-a A is-segal-A a a' ψ) +#def section-arrow-map-fiberwise-equiv uses ( extext funext A is-segal-A a a' ψ) + : Section-arrow A is-segal-A a' a arr-map-fiberwise-equiv + := ( arr-inv-map-fiberwise-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) ``` We see that `#!rzk arrow-map-fiberwise-equiv` has retraction `#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk -#def htpy-comp-map-fib-equiv-inv-map-fib-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses ( A a a' ψ) : ( x : A) → ( homotopy ( hom A a' x) @@ -1234,187 +1166,146 @@ We see that `#!rzk arrow-map-fiberwise-equiv` has retraction ( hom A a' x) ( hom A a x) ( hom A a' x) - ( map-fiberwise-equiv A is-segal-A a a' ψ x) - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ x)) + ( map-fiberwise-equiv x) + ( inv-map-fiberwise-equiv x)) ( identity ( hom A a' x))) - := \ x → second ( second ( inverse-fiberwise-equiv A is-segal-A a a' ψ x)) + := \ x → second ( second ( inverse-fiberwise-equiv x)) ``` We compute the required paths for the retraction of `#!rzk arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) +#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses ( A a a' ψ) + : map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a')) =_{ hom A a' a'} id-hom A a' - := - htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ a' ( id-hom A a') + := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' ( id-hom A a') -#def ap-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) +#def ap-map-fiberwise-equiv uses ( A is-segal-A a a' ψ) + : map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a')) =_{ hom A a' a'} - map-fiberwise-equiv A is-segal-A a a' ψ a' + map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( id-hom A a')) := ap ( hom A a a') ( hom A a' a') - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a')) - ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a')) - ( map-fiberwise-equiv A is-segal-A a a' ψ a') + ( inv-map-fiberwise-equiv a' ( id-hom A a')) + ( comp-is-segal A is-segal-A a a' a' arr-inv-map-fiberwise-equiv (id-hom A a')) + ( map-fiberwise-equiv a') ( eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( inv-map-fiberwise-equiv) ( a') ( id-hom A a')) #def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-fiberwise-equiv A is-segal-A a a' ψ a' + uses ( A is-segal-A a a' ψ) + : map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( id-hom A a')) =_{ hom A a' a'} - map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv := ap ( hom A a a') ( hom A a' a') ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( id-hom A a')) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( map-fiberwise-equiv A is-segal-A a a' ψ a') - ( comp-id-is-segal A is-segal-A a a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( arr-inv-map-fiberwise-equiv) + ( map-fiberwise-equiv a') + ( comp-id-is-segal A is-segal-A a a' arr-inv-map-fiberwise-equiv) #def eq-compute-precomposition-evid-map-fiberwise-equiv - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) - : map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + uses ( A is-segal-A a a' ψ) + : map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv =_{ hom A a' a'} comp-is-segal A is-segal-A a' a a' - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + arr-map-fiberwise-equiv + arr-inv-map-fiberwise-equiv := eq-compute-precomposition-evid funext A is-segal-A a a' - ( map-fiberwise-equiv A is-segal-A a a' ψ) - ( a') - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + map-fiberwise-equiv + a' + arr-inv-map-fiberwise-equiv ``` Concatenate all the paths above. ```rzk -#def eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' uses (funext) - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' + uses ( funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a' a a' - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + arr-map-fiberwise-equiv + arr-inv-map-fiberwise-equiv =_{ hom A a' a'} id-hom A a' := quadruple-concat ( hom A a' a') ( comp-is-segal A is-segal-A a' a a' - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' + arr-map-fiberwise-equiv + arr-inv-map-fiberwise-equiv) + ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) + ( map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) - ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a') + ( arr-inv-map-fiberwise-equiv) ( id-hom A a'))) + ( map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a'))) ( id-hom A a') ( rev ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) + ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) ( comp-is-segal A is-segal-A a' a a' - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( eq-compute-precomposition-evid-map-fiberwise-equiv A is-segal-A a a' ψ)) + arr-map-fiberwise-equiv + arr-inv-map-fiberwise-equiv) + ( eq-compute-precomposition-evid-map-fiberwise-equiv)) ( rev ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map - ( A) - ( is-segal-A) - ( a) - ( a') - ( ψ))) + ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) + ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map)) ( rev ( hom A a' a') - ( map-fiberwise-equiv A is-segal-A a a' ψ a' - ( inv-map-fiberwise-equiv A is-segal-A a a' ψ a' ( id-hom A a'))) - ( map-fiberwise-equiv A is-segal-A a a' ψ a' + ( map-fiberwise-equiv a' + ( inv-map-fiberwise-equiv a' ( id-hom A a'))) + ( map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv) ( id-hom A a'))) - ( ap-map-fiberwise-equiv A is-segal-A a a' ψ)) - ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv A is-segal-A a a' ψ) + ( ap-map-fiberwise-equiv)) + ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv) ``` Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. ```rzk -#def retraction-arrow-map-fiberwise-equiv uses ( funext) - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def retraction-arrow-map-fiberwise-equiv uses ( funext A is-segal-A a a' ψ) : Retraction-arrow A is-segal-A a' a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) := - ( arr-inv-map-fiberwise-equiv A is-segal-A a a' ψ - , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' A is-segal-A a a' ψ) + ( arr-inv-map-fiberwise-equiv + , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a') ``` We show that arrows from fiberwise equivalences are isomorphisms. ```rzk title="RS17, Proposition 10.11 (i)" -#def representable-isomorphism uses ( extext funext) - ( A : U) - ( is-segal-A : is-segal A) - ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) +#def representable-isomorphism uses ( extext funext A is-segal-A a a' ψ) : is-iso-arrow A is-segal-A a' a - ( arr-map-fiberwise-equiv A is-segal-A a a' ψ) + ( arr-map-fiberwise-equiv) := - ( retraction-arrow-map-fiberwise-equiv A is-segal-A a a' ψ - , section-arrow-map-fiberwise-equiv A is-segal-A a a' ψ) + ( retraction-arrow-map-fiberwise-equiv + , section-arrow-map-fiberwise-equiv) + +#end representable-isomorphisms ``` The second part of Proposition 10.11. @@ -1428,6 +1319,6 @@ The second part of Proposition 10.11. : a' = a := eq-iso-is-rezk A is-rezk-A a' a - ( arr-map-fiberwise-equiv A ( first is-rezk-A) a a' ψ - , representable-isomorphism A ( first is-rezk-A) a a' ψ) + ( arr-map-fiberwise-equiv A a a' ψ + , representable-isomorphism A ( first is-rezk-A) a a' ψ) ``` From 1bf1a4e8f47781491414eeb3a6ab8565a4f4dfb0 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Thu, 30 Nov 2023 12:46:10 -0500 Subject: [PATCH 15/20] comment added --- src/simplicial-hott/10-rezk-types.rzk.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 681352c0..4042fcf9 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -1288,19 +1288,18 @@ Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. ```rzk #def retraction-arrow-map-fiberwise-equiv uses ( funext A is-segal-A a a' ψ) - : Retraction-arrow A is-segal-A a' a - ( arr-map-fiberwise-equiv) + : Retraction-arrow A is-segal-A a' a arr-map-fiberwise-equiv := ( arr-inv-map-fiberwise-equiv , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a') ``` -We show that arrows from fiberwise equivalences are isomorphisms. +We show that arrows from fiberwise equivalences are isomorphisms, i.e. that +`#!rzk arr-map-fiberwise-equiv` is an isomorphism. ```rzk title="RS17, Proposition 10.11 (i)" #def representable-isomorphism uses ( extext funext A is-segal-A a a' ψ) - : is-iso-arrow A is-segal-A a' a - ( arr-map-fiberwise-equiv) + : is-iso-arrow A is-segal-A a' a arr-map-fiberwise-equiv := ( retraction-arrow-map-fiberwise-equiv , section-arrow-map-fiberwise-equiv) From ae33cf92e862f27b888e00c6d5e3f341f0217be0 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 12 Dec 2023 17:12:18 +0300 Subject: [PATCH 16/20] Apply autoformatting to 10-rezk-types.rzk.md --- src/simplicial-hott/10-rezk-types.rzk.md | 102 +++++++++++------------ 1 file changed, 51 insertions(+), 51 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 21ddde1c..a91e8e8f 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -953,40 +953,40 @@ equivalence with no extra data, and then define some helpers. #variable A : U #variable is-segal-A : is-segal A #variables a a' : A -#variable ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x)) +#variable ψ : (x : A) → (Equiv (hom A a x) (hom A a' x)) #def map-fiberwise-equiv - : ( x : A) → ( hom A a x) → ( hom A a' x) - := \ x → first ( ψ x) + : ( x : A) → (hom A a x) → (hom A a' x) + := \ x → first (ψ x) #def inverse-fiberwise-equiv - : ( x : A) → ( has-inverse ( hom A a x) ( hom A a' x) ( first ( ψ x))) + : ( x : A) → (has-inverse (hom A a x) (hom A a' x) (first (ψ x))) := \ x → has-inverse-is-equiv ( hom A a x) ( hom A a' x) - ( first ( ψ x)) - ( second ( ψ x)) + ( first (ψ x)) + ( second (ψ x)) -#def inv-map-fiberwise-equiv uses ( A a a' ψ) - : ( x : A) → ( hom A a' x) → ( hom A a x) - := \ x → first ( inverse-fiberwise-equiv x) +#def inv-map-fiberwise-equiv uses (A a a' ψ) + : ( x : A) → (hom A a' x) → (hom A a x) + := \ x → first (inverse-fiberwise-equiv x) #def arr-map-fiberwise-equiv : hom A a' a - := evid A a ( hom A a') ( map-fiberwise-equiv ) + := evid A a (hom A a') (map-fiberwise-equiv) #def arr-inv-map-fiberwise-equiv : hom A a a' - := evid A a' ( hom A a) ( inv-map-fiberwise-equiv) + := evid A a' (hom A a) (inv-map-fiberwise-equiv) ``` We now show that `#!rzk arrow-map-fiberwise-equiv` has section `#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk -#def htpy-inv-map-fib-equiv-map-fib-equiv-id uses ( A a a' ψ) +#def htpy-inv-map-fib-equiv-map-fib-equiv-id uses (A a a' ψ) : ( x : A) → ( homotopy ( hom A a x) @@ -997,8 +997,8 @@ We now show that `#!rzk arrow-map-fiberwise-equiv` has section ( hom A a x) ( inv-map-fiberwise-equiv x) ( map-fiberwise-equiv x)) - ( identity ( hom A a x))) - := \ x → first ( second ( inverse-fiberwise-equiv x)) + ( identity (hom A a x))) + := \ x → first (second (inverse-fiberwise-equiv x)) ``` We compute the required paths for the section of @@ -1006,13 +1006,13 @@ We compute the required paths for the section of ```rzk #def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id - : inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a)) + : inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a)) =_{ hom A a a} id-hom A a - := htpy-inv-map-fib-equiv-map-fib-equiv-id a ( id-hom A a) + := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a) -#def ap-inv-map-fiberwise-equiv uses ( A is-segal-A a a' ψ) - : inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a)) +#def ap-inv-map-fiberwise-equiv uses (A is-segal-A a a' ψ) + : inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a)) =_{ hom A a a} inv-map-fiberwise-equiv a ( comp-is-segal A is-segal-A a' a a @@ -1022,7 +1022,7 @@ We compute the required paths for the section of ap ( hom A a' a) ( hom A a a) - ( map-fiberwise-equiv a ( id-hom A a)) + ( map-fiberwise-equiv a (id-hom A a)) ( comp-is-segal A is-segal-A a' a a ( arr-map-fiberwise-equiv) ( id-hom A a)) @@ -1033,7 +1033,7 @@ We compute the required paths for the section of ( id-hom A a)) #def eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv - uses ( A is-segal-A a a' ψ) + uses (A is-segal-A a a' ψ) : inv-map-fiberwise-equiv a ( comp-is-segal A is-segal-A a' a a ( arr-map-fiberwise-equiv) @@ -1053,7 +1053,7 @@ We compute the required paths for the section of ( id-hom A a)) #def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a - uses ( A is-segal-A a a' ψ) + uses (A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a arr-inv-map-fiberwise-equiv @@ -1071,7 +1071,7 @@ We compute the required paths for the section of ( arr-map-fiberwise-equiv) ( id-hom A a) -#def comp-id-comp-arr-inv-map-arr-map-id-a uses ( A is-segal-A a a' ψ) +#def comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a arr-inv-map-fiberwise-equiv @@ -1092,7 +1092,7 @@ Concatenate all the paths above. ```rzk #def eq-comp-arrow-inv-map-arrow-map-equiv-id-a - uses ( extext funext A is-segal-A a a' ψ) + uses (extext funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a' a arr-inv-map-fiberwise-equiv arr-map-fiberwise-equiv @@ -1111,10 +1111,10 @@ Concatenate all the paths above. ( id-hom A a)) ( comp-is-segal A is-segal-A a a' a ( arr-inv-map-fiberwise-equiv) - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) - ( inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a))) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) + ( inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a))) ( id-hom A a) ( rev ( hom A a a) @@ -1131,16 +1131,16 @@ Concatenate all the paths above. ( rev ( hom A a a) ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) ( comp-is-segal A is-segal-A a a' a ( arr-inv-map-fiberwise-equiv) - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv)) ( rev ( hom A a a) - ( inv-map-fiberwise-equiv a ( map-fiberwise-equiv a ( id-hom A a))) + ( inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a))) ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv ( id-hom A a))) + ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) ( ap-inv-map-fiberwise-equiv)) ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id) ``` @@ -1148,16 +1148,16 @@ Concatenate all the paths above. Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. ```rzk -#def section-arrow-map-fiberwise-equiv uses ( extext funext A is-segal-A a a' ψ) +#def section-arrow-map-fiberwise-equiv uses (extext funext A is-segal-A a a' ψ) : Section-arrow A is-segal-A a' a arr-map-fiberwise-equiv - := ( arr-inv-map-fiberwise-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) + := (arr-inv-map-fiberwise-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) ``` We see that `#!rzk arrow-map-fiberwise-equiv` has retraction `#!rzk arrow-inv-map-fiberwise-equiv`. ```rzk -#def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses ( A a a' ψ) +#def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) : ( x : A) → ( homotopy ( hom A a' x) @@ -1168,22 +1168,22 @@ We see that `#!rzk arrow-map-fiberwise-equiv` has retraction ( hom A a' x) ( map-fiberwise-equiv x) ( inv-map-fiberwise-equiv x)) - ( identity ( hom A a' x))) - := \ x → second ( second ( inverse-fiberwise-equiv x)) + ( identity (hom A a' x))) + := \ x → second (second (inverse-fiberwise-equiv x)) ``` We compute the required paths for the retraction of `#!rzk arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses ( A a a' ψ) - : map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a')) +#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) + : map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a')) =_{ hom A a' a'} id-hom A a' - := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' ( id-hom A a') + := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a') -#def ap-map-fiberwise-equiv uses ( A is-segal-A a a' ψ) - : map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a')) +#def ap-map-fiberwise-equiv uses (A is-segal-A a a' ψ) + : map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a')) =_{ hom A a' a'} map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' @@ -1193,7 +1193,7 @@ We compute the required paths for the retraction of ap ( hom A a a') ( hom A a' a') - ( inv-map-fiberwise-equiv a' ( id-hom A a')) + ( inv-map-fiberwise-equiv a' (id-hom A a')) ( comp-is-segal A is-segal-A a a' a' arr-inv-map-fiberwise-equiv (id-hom A a')) ( map-fiberwise-equiv a') ( eq-compute-precomposition-evid funext A is-segal-A a' a @@ -1202,7 +1202,7 @@ We compute the required paths for the retraction of ( id-hom A a')) #def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map - uses ( A is-segal-A a a' ψ) + uses (A is-segal-A a a' ψ) : map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-fiberwise-equiv) @@ -1221,7 +1221,7 @@ We compute the required paths for the retraction of ( comp-id-is-segal A is-segal-A a a' arr-inv-map-fiberwise-equiv) #def eq-compute-precomposition-evid-map-fiberwise-equiv - uses ( A is-segal-A a a' ψ) + uses (A is-segal-A a a' ψ) : map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv =_{ hom A a' a'} comp-is-segal A is-segal-A a' a a' @@ -1238,7 +1238,7 @@ Concatenate all the paths above. ```rzk #def eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' - uses ( funext A is-segal-A a a' ψ) + uses (funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a' a a' arr-map-fiberwise-equiv arr-inv-map-fiberwise-equiv @@ -1255,7 +1255,7 @@ Concatenate all the paths above. ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-fiberwise-equiv) ( id-hom A a'))) - ( map-fiberwise-equiv a' ( inv-map-fiberwise-equiv a' ( id-hom A a'))) + ( map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a'))) ( id-hom A a') ( rev ( hom A a' a') @@ -1275,7 +1275,7 @@ Concatenate all the paths above. ( rev ( hom A a' a') ( map-fiberwise-equiv a' - ( inv-map-fiberwise-equiv a' ( id-hom A a'))) + ( inv-map-fiberwise-equiv a' (id-hom A a'))) ( map-fiberwise-equiv a' ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-fiberwise-equiv) @@ -1287,7 +1287,7 @@ Concatenate all the paths above. Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. ```rzk -#def retraction-arrow-map-fiberwise-equiv uses ( funext A is-segal-A a a' ψ) +#def retraction-arrow-map-fiberwise-equiv uses (funext A is-segal-A a a' ψ) : Retraction-arrow A is-segal-A a' a arr-map-fiberwise-equiv := ( arr-inv-map-fiberwise-equiv @@ -1298,7 +1298,7 @@ We show that arrows from fiberwise equivalences are isomorphisms, i.e. that `#!rzk arr-map-fiberwise-equiv` is an isomorphism. ```rzk title="RS17, Proposition 10.11 (i)" -#def representable-isomorphism uses ( extext funext A is-segal-A a a' ψ) +#def representable-isomorphism uses (extext funext A is-segal-A a a' ψ) : is-iso-arrow A is-segal-A a' a arr-map-fiberwise-equiv := ( retraction-arrow-map-fiberwise-equiv @@ -1310,14 +1310,14 @@ We show that arrows from fiberwise equivalences are isomorphisms, i.e. that The second part of Proposition 10.11. ```rzk title="RS17, Proposition 10.11 (ii)" -#def eq-representable-isomorphism uses ( extext funext) +#def eq-representable-isomorphism uses (extext funext) ( A : U) ( is-rezk-A : is-rezk A) ( a a' : A) - ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x))) + ( ψ : (x : A) → (Equiv (hom A a x) (hom A a' x))) : a' = a := eq-iso-is-rezk A is-rezk-A a' a ( arr-map-fiberwise-equiv A a a' ψ - , representable-isomorphism A ( first is-rezk-A) a a' ψ) + , representable-isomorphism A (first is-rezk-A) a a' ψ) ``` From be94531cc37d2f68005ca130585169a39319c945 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 14 Dec 2023 19:00:12 -0500 Subject: [PATCH 17/20] name change from fiberwise to representable --- src/simplicial-hott/10-rezk-types.rzk.md | 265 +++++++++++------------ 1 file changed, 132 insertions(+), 133 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index a91e8e8f..7bde9f91 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -944,8 +944,7 @@ In particular, every contractible type is Rezk ## Representable isomorphisms. -We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise -equivalence with no extra data, and then define some helpers. +We prove [RS17, Proposition 10.11]. We first need to access the fiberwise equivalence with no extra data, and then define some helpers. ```rzk #section representable-isomorphisms @@ -955,11 +954,11 @@ equivalence with no extra data, and then define some helpers. #variables a a' : A #variable ψ : (x : A) → (Equiv (hom A a x) (hom A a' x)) -#def map-fiberwise-equiv +#def map-representable-equiv : ( x : A) → (hom A a x) → (hom A a' x) := \ x → first (ψ x) -#def inverse-fiberwise-equiv +#def inverse-representable-equiv : ( x : A) → (has-inverse (hom A a x) (hom A a' x) (first (ψ x))) := \ x → @@ -969,21 +968,21 @@ equivalence with no extra data, and then define some helpers. ( first (ψ x)) ( second (ψ x)) -#def inv-map-fiberwise-equiv uses (A a a' ψ) +#def inv-map-representable-equiv uses (A a a' ψ) : ( x : A) → (hom A a' x) → (hom A a x) - := \ x → first (inverse-fiberwise-equiv x) + := \ x → first (inverse-representable-equiv x) -#def arr-map-fiberwise-equiv +#def arr-map-representable-equiv : hom A a' a - := evid A a (hom A a') (map-fiberwise-equiv) + := evid A a (hom A a') (map-representable-equiv) -#def arr-inv-map-fiberwise-equiv +#def arr-inv-map-representable-equiv : hom A a a' - := evid A a' (hom A a) (inv-map-fiberwise-equiv) + := evid A a' (hom A a) (inv-map-representable-equiv) ``` -We now show that `#!rzk arrow-map-fiberwise-equiv` has section -`#!rzk arrow-inv-map-fiberwise-equiv`. +We now show that `#!rzk arrow-map-representable-equiv` has section +`#!rzk arrow-inv-map-representable-equiv`. ```rzk #def htpy-inv-map-fib-equiv-map-fib-equiv-id uses (A a a' ψ) @@ -995,97 +994,97 @@ We now show that `#!rzk arrow-map-fiberwise-equiv` has section ( hom A a x) ( hom A a' x) ( hom A a x) - ( inv-map-fiberwise-equiv x) - ( map-fiberwise-equiv x)) + ( inv-map-representable-equiv x) + ( map-representable-equiv x)) ( identity (hom A a x))) - := \ x → first (second (inverse-fiberwise-equiv x)) + := \ x → first (second (inverse-representable-equiv x)) ``` We compute the required paths for the section of -`#!rzk arrow-map-fiberwise-equiv`. +`#!rzk arrow-map-representable-equiv`. ```rzk #def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id - : inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a)) + : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) =_{ hom A a a} id-hom A a := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a) -#def ap-inv-map-fiberwise-equiv uses (A is-segal-A a a' ψ) - : inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a)) +#def ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ) + : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) =_{ hom A a a} - inv-map-fiberwise-equiv a + inv-map-representable-equiv a ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) := ap ( hom A a' a) ( hom A a a) - ( map-fiberwise-equiv a (id-hom A a)) + ( map-representable-equiv a (id-hom A a)) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) - ( inv-map-fiberwise-equiv a) + ( inv-map-representable-equiv a) ( eq-compute-precomposition-evid funext A is-segal-A a a' - ( map-fiberwise-equiv) + ( map-representable-equiv) ( a) ( id-hom A a)) -#def eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv +#def eq-compute-precomposition-evid-arr-inv-map-representable-equiv uses (A is-segal-A a a' ψ) - : inv-map-fiberwise-equiv a + : inv-map-representable-equiv a ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) := eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-fiberwise-equiv) + ( inv-map-representable-equiv) ( a) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) #def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a uses (A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( id-hom A a) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( comp-is-segal A is-segal-A a' a a - ( arr-map-fiberwise-equiv) + ( arr-map-representable-equiv) ( id-hom A a)) := associative-is-segal extext A is-segal-A a a' a a - ( arr-inv-map-fiberwise-equiv) - ( arr-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) + ( arr-map-representable-equiv) ( id-hom A a) #def comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( id-hom A a) =_{ hom A a a} comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv + arr-inv-map-representable-equiv + arr-map-representable-equiv := comp-id-is-segal A is-segal-A a a ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ``` Concatenate all the paths above. @@ -1094,67 +1093,67 @@ Concatenate all the paths above. #def eq-comp-arrow-inv-map-arrow-map-equiv-id-a uses (extext funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv + arr-inv-map-representable-equiv + arr-map-representable-equiv =_{ hom A a a} id-hom A a := quintuple-concat ( hom A a a) ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( id-hom A a)) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv) - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) - ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) - ( inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a))) + ( arr-inv-map-representable-equiv) + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) ( id-hom A a) ( rev ( hom A a a) ( comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( id-hom A a)) ( comp-is-segal A is-segal-A a a' a - arr-inv-map-fiberwise-equiv - arr-map-fiberwise-equiv) + arr-inv-map-representable-equiv + arr-map-representable-equiv) ( comp-id-comp-arr-inv-map-arr-map-id-a)) ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a) ( rev ( hom A a a) - ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) + ( inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-fiberwise-equiv) - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) - ( eq-compute-precomposition-evid-arr-inv-map-fiberwise-equiv)) + ( arr-inv-map-representable-equiv) + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( eq-compute-precomposition-evid-arr-inv-map-representable-equiv)) ( rev ( hom A a a) - ( inv-map-fiberwise-equiv a (map-fiberwise-equiv a (id-hom A a))) - ( inv-map-fiberwise-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-fiberwise-equiv (id-hom A a))) - ( ap-inv-map-fiberwise-equiv)) + ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) + ( inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( ap-inv-map-representable-equiv)) ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id) ``` -Now we give the section of `#!rzk arrow-map-fiberwise-equiv`. +Now we give the section of `#!rzk arrow-map-representable-equiv`. ```rzk -#def section-arrow-map-fiberwise-equiv uses (extext funext A is-segal-A a a' ψ) - : Section-arrow A is-segal-A a' a arr-map-fiberwise-equiv - := (arr-inv-map-fiberwise-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) +#def section-arrow-map-representable-equiv uses (extext funext A is-segal-A a a' ψ) + : Section-arrow A is-segal-A a' a arr-map-representable-equiv + := (arr-inv-map-representable-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) ``` -We see that `#!rzk arrow-map-fiberwise-equiv` has retraction -`#!rzk arrow-inv-map-fiberwise-equiv`. +We see that `#!rzk arrow-map-representable-equiv` has retraction +`#!rzk arrow-inv-map-representable-equiv`. ```rzk #def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) @@ -1166,10 +1165,10 @@ We see that `#!rzk arrow-map-fiberwise-equiv` has retraction ( hom A a' x) ( hom A a x) ( hom A a' x) - ( map-fiberwise-equiv x) - ( inv-map-fiberwise-equiv x)) + ( map-representable-equiv x) + ( inv-map-representable-equiv x)) ( identity (hom A a' x))) - := \ x → second (second (inverse-fiberwise-equiv x)) + := \ x → second (second (inverse-representable-equiv x)) ``` We compute the required paths for the retraction of @@ -1177,132 +1176,132 @@ We compute the required paths for the retraction of ```rzk #def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) - : map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a')) + : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) =_{ hom A a' a'} id-hom A a' := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a') -#def ap-map-fiberwise-equiv uses (A is-segal-A a a' ψ) - : map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a')) +#def ap-map-representable-equiv uses (A is-segal-A a a' ψ) + : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) =_{ hom A a' a'} - map-fiberwise-equiv a' + map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a')) := ap ( hom A a a') ( hom A a' a') - ( inv-map-fiberwise-equiv a' (id-hom A a')) - ( comp-is-segal A is-segal-A a a' a' arr-inv-map-fiberwise-equiv (id-hom A a')) - ( map-fiberwise-equiv a') + ( inv-map-representable-equiv a' (id-hom A a')) + ( comp-is-segal A is-segal-A a a' a' arr-inv-map-representable-equiv (id-hom A a')) + ( map-representable-equiv a') ( eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-fiberwise-equiv) + ( inv-map-representable-equiv) ( a') ( id-hom A a')) -#def ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map +#def ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map uses (A is-segal-A a a' ψ) - : map-fiberwise-equiv a' + : map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a')) =_{ hom A a' a'} - map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv + map-representable-equiv a' arr-inv-map-representable-equiv := ap ( hom A a a') ( hom A a' a') ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a')) - ( arr-inv-map-fiberwise-equiv) - ( map-fiberwise-equiv a') - ( comp-id-is-segal A is-segal-A a a' arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) + ( map-representable-equiv a') + ( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv) -#def eq-compute-precomposition-evid-map-fiberwise-equiv +#def eq-compute-precomposition-evid-map-representable-equiv uses (A is-segal-A a a' ψ) - : map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv + : map-representable-equiv a' arr-inv-map-representable-equiv =_{ hom A a' a'} comp-is-segal A is-segal-A a' a a' - arr-map-fiberwise-equiv - arr-inv-map-fiberwise-equiv + arr-map-representable-equiv + arr-inv-map-representable-equiv := eq-compute-precomposition-evid funext A is-segal-A a a' - map-fiberwise-equiv + map-representable-equiv a' - arr-inv-map-fiberwise-equiv + arr-inv-map-representable-equiv ``` Concatenate all the paths above. ```rzk -#def eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a' +#def eq-comp-arr-map-representable-arr-inv-map-representable-id-a' uses (funext A is-segal-A a a' ψ) : comp-is-segal A is-segal-A a' a a' - arr-map-fiberwise-equiv - arr-inv-map-fiberwise-equiv + arr-map-representable-equiv + arr-inv-map-representable-equiv =_{ hom A a' a'} id-hom A a' := quadruple-concat ( hom A a' a') ( comp-is-segal A is-segal-A a' a a' - arr-map-fiberwise-equiv - arr-inv-map-fiberwise-equiv) - ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) - ( map-fiberwise-equiv a' + arr-map-representable-equiv + arr-inv-map-representable-equiv) + ( map-representable-equiv a' arr-inv-map-representable-equiv) + ( map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a'))) - ( map-fiberwise-equiv a' (inv-map-fiberwise-equiv a' (id-hom A a'))) + ( map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))) ( id-hom A a') ( rev ( hom A a' a') - ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) + ( map-representable-equiv a' arr-inv-map-representable-equiv) ( comp-is-segal A is-segal-A a' a a' - arr-map-fiberwise-equiv - arr-inv-map-fiberwise-equiv) - ( eq-compute-precomposition-evid-map-fiberwise-equiv)) + arr-map-representable-equiv + arr-inv-map-representable-equiv) + ( eq-compute-precomposition-evid-map-representable-equiv)) ( rev ( hom A a' a') - ( map-fiberwise-equiv a' + ( map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a'))) - ( map-fiberwise-equiv a' arr-inv-map-fiberwise-equiv) - ( ap-map-fiberwise-equiv-eq-arr-inv-map-id-a'-arr-inv-map)) + ( map-representable-equiv a' arr-inv-map-representable-equiv) + ( ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map)) ( rev ( hom A a' a') - ( map-fiberwise-equiv a' - ( inv-map-fiberwise-equiv a' (id-hom A a'))) - ( map-fiberwise-equiv a' + ( map-representable-equiv a' + ( inv-map-representable-equiv a' (id-hom A a'))) + ( map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-fiberwise-equiv) + ( arr-inv-map-representable-equiv) ( id-hom A a'))) - ( ap-map-fiberwise-equiv)) + ( ap-map-representable-equiv)) ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv) ``` -Now we give the retraction of `#!rzk arrow-map-fiberwise-equiv`. +Now we give the retraction of `#!rzk arrow-map-representable-equiv`. ```rzk -#def retraction-arrow-map-fiberwise-equiv uses (funext A is-segal-A a a' ψ) - : Retraction-arrow A is-segal-A a' a arr-map-fiberwise-equiv +#def retraction-arrow-map-representable-equiv uses (funext A is-segal-A a a' ψ) + : Retraction-arrow A is-segal-A a' a arr-map-representable-equiv := - ( arr-inv-map-fiberwise-equiv - , eq-comp-arr-map-fiberwise-arr-inv-map-fiberwise-id-a') + ( arr-inv-map-representable-equiv + , eq-comp-arr-map-representable-arr-inv-map-representable-id-a') ``` -We show that arrows from fiberwise equivalences are isomorphisms, i.e. that -`#!rzk arr-map-fiberwise-equiv` is an isomorphism. +We show that arrows from representable equivalences are isomorphisms, i.e. that +`#!rzk arr-map-representable-equiv` is an isomorphism. ```rzk title="RS17, Proposition 10.11 (i)" #def representable-isomorphism uses (extext funext A is-segal-A a a' ψ) - : is-iso-arrow A is-segal-A a' a arr-map-fiberwise-equiv + : is-iso-arrow A is-segal-A a' a arr-map-representable-equiv := - ( retraction-arrow-map-fiberwise-equiv - , section-arrow-map-fiberwise-equiv) + ( retraction-arrow-map-representable-equiv + , section-arrow-map-representable-equiv) #end representable-isomorphisms ``` @@ -1318,6 +1317,6 @@ The second part of Proposition 10.11. : a' = a := eq-iso-is-rezk A is-rezk-A a' a - ( arr-map-fiberwise-equiv A a a' ψ + ( arr-map-representable-equiv A a a' ψ , representable-isomorphism A (first is-rezk-A) a a' ψ) ``` From 40143806e45d40ef7ab69308b6413af50747d518 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 14 Dec 2023 19:14:48 -0500 Subject: [PATCH 18/20] moved some reversals to the local paths --- src/simplicial-hott/10-rezk-types.rzk.md | 133 ++++++++++++----------- 1 file changed, 67 insertions(+), 66 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 7bde9f91..0b5dd647 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -944,7 +944,8 @@ In particular, every contractible type is Rezk ## Representable isomorphisms. -We prove [RS17, Proposition 10.11]. We first need to access the fiberwise equivalence with no extra data, and then define some helpers. +We prove [RS17, Proposition 10.11]. We first need to access the fiberwise +equivalence with no extra data, and then define some helpers. ```rzk #section representable-isomorphisms @@ -1010,46 +1011,58 @@ We compute the required paths for the section of id-hom A a := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a) -#def ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ) - : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) - =_{ hom A a a} - inv-map-representable-equiv a +#def rev-ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ) + : inv-map-representable-equiv a ( comp-is-segal A is-segal-A a' a a ( arr-map-representable-equiv) ( id-hom A a)) + =_{ hom A a a} + inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) := - ap - ( hom A a' a) - ( hom A a a) - ( map-representable-equiv a (id-hom A a)) - ( comp-is-segal A is-segal-A a' a a - ( arr-map-representable-equiv) - ( id-hom A a)) - ( inv-map-representable-equiv a) - ( eq-compute-precomposition-evid funext A is-segal-A a a' - ( map-representable-equiv) - ( a) - ( id-hom A a)) + rev + ( hom A a a) + ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) + ( inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( ap + ( hom A a' a) + ( hom A a a) + ( map-representable-equiv a (id-hom A a)) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-representable-equiv) + ( id-hom A a)) + ( inv-map-representable-equiv a) + ( eq-compute-precomposition-evid funext A is-segal-A a a' + ( map-representable-equiv) + ( a) + ( id-hom A a))) -#def eq-compute-precomposition-evid-arr-inv-map-representable-equiv +#def rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv uses (A is-segal-A a a' ψ) - : inv-map-representable-equiv a - ( comp-is-segal A is-segal-A a' a a - ( arr-map-representable-equiv) - ( id-hom A a)) - =_{ hom A a a} - comp-is-segal A is-segal-A a a' a + : comp-is-segal A is-segal-A a a' a ( arr-inv-map-representable-equiv) ( comp-is-segal A is-segal-A a' a a ( arr-map-representable-equiv) ( id-hom A a)) + =_{ hom A a a} + inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a + ( arr-map-representable-equiv) + ( id-hom A a)) := - eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-representable-equiv) - ( a) - ( comp-is-segal A is-segal-A a' a a - ( arr-map-representable-equiv) - ( id-hom A a)) + rev + ( hom A a a) + ( inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( comp-is-segal A is-segal-A a a' a + ( arr-inv-map-representable-equiv) + ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) + ( eq-compute-precomposition-evid funext A is-segal-A a' a + ( inv-map-representable-equiv) + ( a) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-representable-equiv) + ( id-hom A a))) #def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a uses (A is-segal-A a a' ψ) @@ -1070,21 +1083,31 @@ We compute the required paths for the section of ( arr-map-representable-equiv) ( id-hom A a) -#def comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) - : comp-is-segal A is-segal-A a a a +#def rev-comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) + : comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv + ( id-hom A a) + =_{ hom A a a} + comp-is-segal A is-segal-A a a a ( comp-is-segal A is-segal-A a a' a arr-inv-map-representable-equiv arr-map-representable-equiv) - ( id-hom A a) - =_{ hom A a a} - comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv := - comp-id-is-segal A is-segal-A a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) + rev + ( hom A a a) + ( comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( id-hom A a)) + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( comp-id-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv)) ``` Concatenate all the paths above. @@ -1115,32 +1138,10 @@ Concatenate all the paths above. ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) ( id-hom A a) - ( rev - ( hom A a a) - ( comp-is-segal A is-segal-A a a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - ( id-hom A a)) - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - ( comp-id-comp-arr-inv-map-arr-map-id-a)) + ( rev-comp-id-comp-arr-inv-map-arr-map-id-a) ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a) - ( rev - ( hom A a a) - ( inv-map-representable-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) - ( comp-is-segal A is-segal-A a a' a - ( arr-inv-map-representable-equiv) - ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) - ( eq-compute-precomposition-evid-arr-inv-map-representable-equiv)) - ( rev - ( hom A a a) - ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) - ( inv-map-representable-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) - ( ap-inv-map-representable-equiv)) + ( rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv) + ( rev-ap-inv-map-representable-equiv) ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id) ``` From 99177975b9431b6be72ef77b59986ea578ed97ce Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 14 Dec 2023 19:40:26 -0500 Subject: [PATCH 19/20] moved around the revs --- src/simplicial-hott/10-rezk-types.rzk.md | 232 +++++++++++------------ 1 file changed, 116 insertions(+), 116 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 0b5dd647..e41a0e54 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -1005,37 +1005,50 @@ We compute the required paths for the section of `#!rzk arrow-map-representable-equiv`. ```rzk -#def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id - : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) - =_{ hom A a a} - id-hom A a - := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a) - -#def rev-ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ) - : inv-map-representable-equiv a - ( comp-is-segal A is-segal-A a' a a - ( arr-map-representable-equiv) - ( id-hom A a)) +#def rev-comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) + : comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv =_{ hom A a a} - inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) + comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( id-hom A a) := rev ( hom A a a) - ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))) - ( inv-map-representable-equiv a - ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a))) - ( ap - ( hom A a' a) - ( hom A a a) - ( map-representable-equiv a (id-hom A a)) + ( comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( id-hom A a)) + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( comp-id-is-segal A is-segal-A a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv)) + +#def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a + uses (A is-segal-A a a' ψ) + : comp-is-segal A is-segal-A a a a + ( comp-is-segal A is-segal-A a a' a + arr-inv-map-representable-equiv + arr-map-representable-equiv) + ( id-hom A a) + =_{ hom A a a} + comp-is-segal A is-segal-A a a' a + ( arr-inv-map-representable-equiv) ( comp-is-segal A is-segal-A a' a a ( arr-map-representable-equiv) ( id-hom A a)) - ( inv-map-representable-equiv a) - ( eq-compute-precomposition-evid funext A is-segal-A a a' - ( map-representable-equiv) - ( a) - ( id-hom A a))) + := + associative-is-segal extext A is-segal-A a a' a a + ( arr-inv-map-representable-equiv) + ( arr-map-representable-equiv) + ( id-hom A a) #def rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv uses (A is-segal-A a a' ψ) @@ -1064,50 +1077,37 @@ We compute the required paths for the section of ( arr-map-representable-equiv) ( id-hom A a))) -#def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a - uses (A is-segal-A a a' ψ) - : comp-is-segal A is-segal-A a a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - ( id-hom A a) +#def rev-ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ) + : inv-map-representable-equiv a + ( comp-is-segal A is-segal-A a' a a + ( arr-map-representable-equiv) + ( id-hom A a)) =_{ hom A a a} - comp-is-segal A is-segal-A a a' a - ( arr-inv-map-representable-equiv) - ( comp-is-segal A is-segal-A a' a a + inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) + := + ap + ( hom A a' a) + ( hom A a a) + ( comp-is-segal A is-segal-A a' a a ( arr-map-representable-equiv) ( id-hom A a)) - := - associative-is-segal extext A is-segal-A a a' a a - ( arr-inv-map-representable-equiv) - ( arr-map-representable-equiv) - ( id-hom A a) + ( map-representable-equiv a (id-hom A a)) + ( inv-map-representable-equiv a) + ( rev (hom A a' a) + ( map-representable-equiv a (id-hom A a)) + ( comp-is-segal A is-segal-A a' a a + ( arr-map-representable-equiv) + ( id-hom A a)) + ( eq-compute-precomposition-evid funext A is-segal-A a a' + ( map-representable-equiv) + ( a) + ( id-hom A a))) -#def rev-comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ) - : comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv - ( id-hom A a) +#def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id + : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)) =_{ hom A a a} - comp-is-segal A is-segal-A a a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - := - rev - ( hom A a a) - ( comp-is-segal A is-segal-A a a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - ( id-hom A a)) - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv) - ( comp-id-is-segal A is-segal-A a a a - ( comp-is-segal A is-segal-A a a' a - arr-inv-map-representable-equiv - arr-map-representable-equiv)) + id-hom A a + := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a) ``` Concatenate all the paths above. @@ -1150,7 +1150,8 @@ Now we give the section of `#!rzk arrow-map-representable-equiv`. ```rzk #def section-arrow-map-representable-equiv uses (extext funext A is-segal-A a a' ψ) : Section-arrow A is-segal-A a' a arr-map-representable-equiv - := (arr-inv-map-representable-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) + := + ( arr-inv-map-representable-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a) ``` We see that `#!rzk arrow-map-representable-equiv` has retraction @@ -1176,14 +1177,28 @@ We compute the required paths for the retraction of `#!rzk arrow-map-iso-representable`. ```rzk -#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) - : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) +#def rev-eq-compute-precomposition-evid-map-representable-equiv + uses (A is-segal-A a a' ψ) + : comp-is-segal A is-segal-A a' a a' + arr-map-representable-equiv + arr-inv-map-representable-equiv =_{ hom A a' a'} - id-hom A a' - := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a') + map-representable-equiv a' arr-inv-map-representable-equiv + := + rev + ( hom A a' a') + ( map-representable-equiv a' arr-inv-map-representable-equiv) + ( comp-is-segal A is-segal-A a' a a' + arr-map-representable-equiv + arr-inv-map-representable-equiv) + ( eq-compute-precomposition-evid funext A is-segal-A a a' + map-representable-equiv + a' + arr-inv-map-representable-equiv) -#def ap-map-representable-equiv uses (A is-segal-A a a' ψ) - : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) +#def rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map + uses (A is-segal-A a a' ψ) + : map-representable-equiv a' arr-inv-map-representable-equiv =_{ hom A a' a'} map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' @@ -1193,22 +1208,26 @@ We compute the required paths for the retraction of ap ( hom A a a') ( hom A a' a') - ( inv-map-representable-equiv a' (id-hom A a')) - ( comp-is-segal A is-segal-A a a' a' arr-inv-map-representable-equiv (id-hom A a')) - ( map-representable-equiv a') - ( eq-compute-precomposition-evid funext A is-segal-A a' a - ( inv-map-representable-equiv) - ( a') + ( arr-inv-map-representable-equiv) + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-representable-equiv) ( id-hom A a')) + ( map-representable-equiv a') + ( rev + ( hom A a a') + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-representable-equiv) + ( id-hom A a')) + ( arr-inv-map-representable-equiv) + ( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv)) -#def ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map - uses (A is-segal-A a a' ψ) +#def ap-map-representable-equiv uses (A is-segal-A a a' ψ) : map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-representable-equiv) ( id-hom A a')) =_{ hom A a' a'} - map-representable-equiv a' arr-inv-map-representable-equiv + map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) := ap ( hom A a a') @@ -1216,22 +1235,24 @@ We compute the required paths for the retraction of ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-representable-equiv) ( id-hom A a')) - ( arr-inv-map-representable-equiv) + ( inv-map-representable-equiv a' (id-hom A a')) ( map-representable-equiv a') - ( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv) + ( rev + ( hom A a a') + ( inv-map-representable-equiv a' (id-hom A a')) + ( comp-is-segal A is-segal-A a a' a' + ( arr-inv-map-representable-equiv) + ( id-hom A a')) + ( eq-compute-precomposition-evid funext A is-segal-A a' a + ( inv-map-representable-equiv) + ( a') + ( id-hom A a'))) -#def eq-compute-precomposition-evid-map-representable-equiv - uses (A is-segal-A a a' ψ) - : map-representable-equiv a' arr-inv-map-representable-equiv +#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ) + : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')) =_{ hom A a' a'} - comp-is-segal A is-segal-A a' a a' - arr-map-representable-equiv - arr-inv-map-representable-equiv - := - eq-compute-precomposition-evid funext A is-segal-A a a' - map-representable-equiv - a' - arr-inv-map-representable-equiv + id-hom A a' + := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a') ``` Concatenate all the paths above. @@ -1257,30 +1278,9 @@ Concatenate all the paths above. ( id-hom A a'))) ( map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))) ( id-hom A a') - ( rev - ( hom A a' a') - ( map-representable-equiv a' arr-inv-map-representable-equiv) - ( comp-is-segal A is-segal-A a' a a' - arr-map-representable-equiv - arr-inv-map-representable-equiv) - ( eq-compute-precomposition-evid-map-representable-equiv)) - ( rev - ( hom A a' a') - ( map-representable-equiv a' - ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-representable-equiv) - ( id-hom A a'))) - ( map-representable-equiv a' arr-inv-map-representable-equiv) - ( ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map)) - ( rev - ( hom A a' a') - ( map-representable-equiv a' - ( inv-map-representable-equiv a' (id-hom A a'))) - ( map-representable-equiv a' - ( comp-is-segal A is-segal-A a a' a' - ( arr-inv-map-representable-equiv) - ( id-hom A a'))) - ( ap-map-representable-equiv)) + ( rev-eq-compute-precomposition-evid-map-representable-equiv) + ( rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map) + ( rev-ap-map-representable-equiv) ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv) ``` From 06abed021605ece4c6a38e0e4086feeaf5cd2b83 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 14 Dec 2023 19:42:38 -0500 Subject: [PATCH 20/20] typo --- src/simplicial-hott/10-rezk-types.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index e41a0e54..af92baa0 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -1221,7 +1221,7 @@ We compute the required paths for the retraction of ( arr-inv-map-representable-equiv) ( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv)) -#def ap-map-representable-equiv uses (A is-segal-A a a' ψ) +#def rev-ap-map-representable-equiv uses (A is-segal-A a a' ψ) : map-representable-equiv a' ( comp-is-segal A is-segal-A a a' a' ( arr-inv-map-representable-equiv)