From 4b2eb30393c4f1bfafe07af5194d964e397d4312 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Fri, 20 Oct 2023 19:10:21 -0400 Subject: [PATCH 1/7] constructed an automorphism between the object part of two unit components --- src/simplicial-hott/05-segal-types.rzk.md | 14 ++ .../06-2cat-of-segal-types.rzk.md | 24 ++ src/simplicial-hott/08-covariant.rzk.md | 2 +- src/simplicial-hott/11-adjunctions.rzk.md | 210 ++++++++++++++++++ 4 files changed, 249 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index 6a0b1166..56e511b4 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -1160,6 +1160,20 @@ We conclude that Segal composition is associative. ( left-associative-is-segal A is-segal-A w x y z f g h) ( right-associative-is-segal A is-segal-A w x y z f g h) +#def rev-associative-is-segal uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( w x y z : A) + ( f : hom A w x) + ( g : hom A x y) + ( h : hom A y z) + : ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h)) = + ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h) + := + rev (hom A w z) + ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h) + ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h)) + ( associative-is-segal A is-segal-A w x y z f g h) #def postcomp-is-segal ( A : U) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 85ddd775..a2a6dd7a 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -101,6 +101,30 @@ Preservation of composition requires the Segal hypothesis. ( ap-hom2 A B F x y z f g ( comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g)) + +#def rev-functors-pres-comp + ( A B : U) + ( is-segal-A : is-segal A) + ( is-segal-B : is-segal B) + ( F : A → B) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + : + ( ap-hom A B F x z (comp-is-segal A is-segal-A x y z f g)) + = + ( comp-is-segal B is-segal-B + ( F x) (F y) (F z) + ( ap-hom A B F x y f) + ( ap-hom A B F y z g)) + := + rev (hom B (F x) (F z)) + ( comp-is-segal B is-segal-B + ( F x) (F y) (F z) + ( ap-hom A B F x y f) + ( ap-hom A B F y z g)) + ( ap-hom A B F x z (comp-is-segal A is-segal-A x y z f g)) + ( functors-pres-comp A B is-segal-A is-segal-B F x y z f g) ``` ## Natural transformations diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 5647968d..ec8cb7a9 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2197,7 +2197,7 @@ The fibers of a covariant fibration over a Segal type are discrete types. ( v)) ``` -In a segal type, covariant hom families are covariant,hence representable homs +In a Segal type, covariant hom families are covariant, hence representable homs are discrete. ```rzk title="RS17, Corollary 8.19" diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index 7ca55ebc..ec14e9c6 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -10,6 +10,7 @@ Some of the definitions in this file rely on function extensionality: ```rzk #assume funext : FunExt +#assume extext : ExtExt ``` ## Transposing adjunctions @@ -1308,3 +1309,212 @@ The calculation for the other triangle identity is dual. #end triangle-identities ``` + +## Adjunctions between Rezk types + +Given a functor `#!rzk u : B → A` from a Rezk type to a Segal type, we show that +the type given by functors `#!rzk f : A → B` and unit transformations that +induce a transposing equivalence is a proposition. This data is nearly the data +of `#!rzk is-transposing-right-adj A B u` + +```rzk +#section all-unit-arrows-equal-is-rezk-is-segal + +#variables A B : U +#variable is-segal-A : is-segal A +#variable is-rezk-B : is-rezk B +#variable u : B → A +#variable a : A +#variables fa fa' : B +#variable ηa : hom A a (u fa) +#variable ηa' : hom A a (u fa') + +#def ηa-transposition + ( b : B) + ( k : hom B fa b) + : (hom A a (u b)) + := comp-is-segal A is-segal-A a (u fa) (u b) ηa (ap-hom B A u fa b k) + +#def ηa'-transposition + ( b : B) + ( k : hom B fa' b) + : (hom A a (u b)) + := comp-is-segal A is-segal-A a (u fa') (u b) ηa' (ap-hom B A u fa' b k) + +#variable ω : (b : B) → is-equiv (hom B fa b) (hom A a (u b)) (ηa-transposition b) + +#variable ω' : (b : B) → is-equiv (hom B fa' b) (hom A a (u b)) (ηa'-transposition b) + +#def to-left-adjoint-components-is-rezk-is-segal uses (A is-segal-A u a ηa) + : hom B fa fa' + := + ( section-is-equiv (hom B fa fa') (hom A a (u fa')) + ( ηa-transposition fa') (ω fa')) + ( ηa') + +#def triangle-to-left-adjoint-components-is-rezk-is-segal + : comp-is-segal A is-segal-A a (u fa) (u fa') + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)) = + ( ηa') + := + ( second + ( has-section-is-equiv (hom B fa fa') (hom A a (u fa')) + ( ηa-transposition fa') (ω fa'))) + ( ηa') + +#def from-left-adjoint-components-is-rezk-is-segal uses (A is-segal-A u a ηa') + : hom B fa' fa + := + ( section-is-equiv (hom B fa' fa) (hom A a (u fa)) + ( ηa'-transposition fa) (ω' fa)) + ( ηa) + +#def triangle-from-left-adjoint-components-is-rezk-is-segal + : comp-is-segal A is-segal-A a (u fa') (u fa) + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)) = + ( ηa) + := + ( second + ( has-section-is-equiv (hom B fa' fa) (hom A a (u fa)) + ( ηa'-transposition fa) (ω' fa))) + ( ηa) + +#def ηa-automorphism uses (extext ω ω') + : comp-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( ap-hom B A u fa fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal))) = ηa + := + quadruple-concat (hom A a (u fa)) + ( comp-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( ap-hom B A u fa fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( ηa) + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( ap-hom B A u fa fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A + ( u) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal))) + ( rev-associative-is-segal extext A is-segal-A a (u fa) (u fa') (u fa) + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa') (u fa) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)) + ( triangle-to-left-adjoint-components-is-rezk-is-segal)) + ( triangle-from-left-adjoint-components-is-rezk-is-segal) + +#def ηa'-automorphism uses (extext ω ω') + : comp-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( ap-hom B A u fa' fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal))) = ηa' + := + quadruple-concat (hom A a (u fa')) + ( comp-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( ap-hom B A u fa' fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( ηa') + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( ap-hom B A u fa' fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A + ( u) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal))) + ( rev-associative-is-segal extext A is-segal-A a + ( u fa') (u fa) (u fa') + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal))) + ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa) (u fa') + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( ηa') + ( ap-hom B A u fa' fa + ( from-left-adjoint-components-is-rezk-is-segal))) + ( ηa) + ( ap-hom B A u fa fa' + ( to-left-adjoint-components-is-rezk-is-segal)) + ( triangle-from-left-adjoint-components-is-rezk-is-segal)) + ( triangle-to-left-adjoint-components-is-rezk-is-segal) + +#end all-unit-arrows-equal-is-rezk-is-segal +``` From a7f89daee16526e75d7f9890e5c1c0b19a41c137 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Fri, 20 Oct 2023 21:24:05 -0400 Subject: [PATCH 2/7] commiting before battery dies --- src/simplicial-hott/10-rezk-types.rzk.md | 14 ++++ src/simplicial-hott/11-adjunctions.rzk.md | 84 +++++++++++++++++++++++ 2 files changed, 98 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index ea9f382c..f4f42770 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -742,6 +742,20 @@ map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence. is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y) ``` +The inverse to `#!rzk iso-eq` for a Rezk type. + +```rzk +#def eq-iso-is-rezk + ( A : U) + ( is-rezk-A : is-rezk A) + ( x y : A) + : Iso A (first is-rezk-A) x y → x = y + := + section-is-equiv (x = y) (Iso A (first is-rezk-A) x y) + ( iso-eq A (first is-rezk-A) x y) + ( ( second is-rezk-A) x y) +``` + The following results show how `#!rzk iso-eq` mediates between the type-theoretic operations on paths and the category-theoretic operations on arrows. diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index ec14e9c6..8c5b9f82 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -1516,5 +1516,89 @@ of `#!rzk is-transposing-right-adj A B u` ( triangle-from-left-adjoint-components-is-rezk-is-segal)) ( triangle-to-left-adjoint-components-is-rezk-is-segal) +#def eq-id-from-to-left-adjoint-components-is-rezk-is-segal uses (extext ηa' ω ω') + : ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal)) = + ( id-hom B fa) + := + inv-ap-is-emb + ( hom B fa fa) + ( hom A a (u fa)) + ( ηa-transposition fa) + ( is-emb-is-equiv + ( hom B fa fa) + ( hom A a (u fa)) + ( ηa-transposition fa) + ( ω fa)) + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal)) + ( id-hom B fa) + ( zig-zag-concat (hom A a (u fa)) + ( ηa-transposition fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal))) + ( ηa) + ( ηa-transposition fa (id-hom B fa)) + ( ηa-automorphism) + ( concat (hom A a (u fa)) + ( ηa-transposition fa (id-hom B fa)) + ( comp-is-segal A is-segal-A a (u fa) (u fa) ηa (id-hom A (u fa))) + ( ηa) + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) ηa + ( ap-hom B A u fa fa (id-hom B fa)) + ( id-hom A (u fa)) + (functors-pres-id extext B A u fa)) + ( comp-id-is-segal A is-segal-A a (u fa) ηa))) + +#def eq-id-to-from-left-adjoint-components-is-rezk-is-segal uses (extext ηa ω ω') + : ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal)) = + ( id-hom B fa') + := + inv-ap-is-emb + ( hom B fa' fa') + ( hom A a (u fa')) + ( ηa'-transposition fa') + ( is-emb-is-equiv + ( hom B fa' fa') + ( hom A a (u fa')) + ( ηa'-transposition fa') + ( ω' fa')) + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal)) + ( id-hom B fa') + ( zig-zag-concat (hom A a (u fa')) + ( ηa'-transposition fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal))) + ( ηa') + ( ηa'-transposition fa' (id-hom B fa')) + ( ηa'-automorphism) + ( concat (hom A a (u fa')) + ( ηa'-transposition fa' (id-hom B fa')) + ( comp-is-segal A is-segal-A a (u fa') (u fa') ηa' (id-hom A (u fa'))) + ( ηa') + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') ηa' + ( ap-hom B A u fa' fa' (id-hom B fa')) + ( id-hom A (u fa')) + (functors-pres-id extext B A u fa')) + ( comp-id-is-segal A is-segal-A a (u fa') ηa'))) + +#def all-left-adjoint-components-eq-is-rezk-is-segal + : fa = fa' + := + eq-iso-is-rezk B is-rezk-B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal, + (( from-left-adjoint-components-is-rezk-is-segal, + eq-id-from-to-left-adjoint-components-is-rezk-is-segal), + ( from-left-adjoint-components-is-rezk-is-segal, + eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) + #end all-unit-arrows-equal-is-rezk-is-segal ``` From d6502c480d4c2a595bd1c52ca35019bb6f70a22c Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sat, 21 Oct 2023 01:38:06 -0400 Subject: [PATCH 3/7] just landed --- src/simplicial-hott/08-covariant.rzk.md | 19 ++++ src/simplicial-hott/10-rezk-types.rzk.md | 18 ++++ src/simplicial-hott/11-adjunctions.rzk.md | 121 +++++++++++++++++++++- 3 files changed, 157 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index ec8cb7a9..fec452d9 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1335,6 +1335,25 @@ equivalence. This follows from the fact that the total types (summed over v ``` +We compute covariant transport of a substitution. + +```rzk +#def compute-covariant-transport-of-substitution + ( A B : U) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( g : B → A) + ( x y : B) + ( f : hom B x y) + ( u : C (g x)) + : covariant-transport B x y f (\ b → C (g b)) + ( is-covariant-substitution-is-covariant A B C is-covariant-C g) u + = + covariant-transport A (g x) (g y) (ap-hom B A g x y f) C + ( is-covariant-C) u + := refl +``` + ## Covariant functoriality The covariant transport operation defines a covariantly functorial action of diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index f4f42770..0c426fec 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -754,6 +754,24 @@ The inverse to `#!rzk iso-eq` for a Rezk type. section-is-equiv (x = y) (Iso A (first is-rezk-A) x y) ( iso-eq A (first is-rezk-A) x y) ( ( second is-rezk-A) x y) + +#def iso-eq-iso-is-rezk + ( A : U) + ( is-rezk-A : is-rezk A) + ( x y : A) + ( (e, is-iso-e) : Iso A (first is-rezk-A) x y) + : first (iso-eq A (first is-rezk-A) x y (eq-iso-is-rezk A is-rezk-A x y (e, is-iso-e))) = e + := + first-path-Σ + ( hom A x y) + ( is-iso-arrow A (first is-rezk-A) x y) + ( iso-eq A (first is-rezk-A) x y + ( eq-iso-is-rezk A is-rezk-A x y (e, is-iso-e))) + ( (e, is-iso-e)) + ( ( second + ( has-section-is-equiv (x = y) (Iso A (first is-rezk-A) x y) + ( iso-eq A (first is-rezk-A) x y) + ( ( second is-rezk-A) x y))) (e, is-iso-e)) ``` The following results show how `#!rzk iso-eq` mediates between the diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index 8c5b9f82..f39354e2 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -1590,7 +1590,7 @@ of `#!rzk is-transposing-right-adj A B u` (functors-pres-id extext B A u fa')) ( comp-id-is-segal A is-segal-A a (u fa') ηa'))) -#def all-left-adjoint-components-eq-is-rezk-is-segal +#def all-left-adjoint-components-equal-is-rezk-is-segal uses (extext A is-segal-A u a ηa ηa' ω ω') : fa = fa' := eq-iso-is-rezk B is-rezk-B fa fa' @@ -1600,5 +1600,124 @@ of `#!rzk is-transposing-right-adj A B u` ( from-left-adjoint-components-is-rezk-is-segal, eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) +#def rev-lem-10-7-application uses (extext ηa' ω ω') + : transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = + covariant-transport B fa fa' + ( first + ( iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa) + := + rev (hom A a (u fa')) + ( covariant-transport B fa fa' + ( first + ( iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + ( compute-covariant-transport-of-hom-family-iso-eq-is-segal B + ( first is-rezk-B) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( fa) + ( fa') + ( all-left-adjoint-components-equal-is-rezk-is-segal) + ( ηa)) + +#def iso-eq-iso-is-rezk-application uses (extext A is-segal-A u a ηa ηa' ω ω') + : first (iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal)) + = to-left-adjoint-components-is-rezk-is-segal + := + iso-eq-iso-is-rezk B is-rezk-B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal, + ( ( from-left-adjoint-components-is-rezk-is-segal, + eq-id-from-to-left-adjoint-components-is-rezk-is-segal), + ( from-left-adjoint-components-is-rezk-is-segal, + eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) + +#def rev-lem-10-7-application' uses (extext ηa' ω ω') + : transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = + covariant-transport B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa) + := + concat (hom A a (u fa')) + ( transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + ( covariant-transport B fa fa' + ( first + ( iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( covariant-transport B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( rev-lem-10-7-application) + ( ap (hom B fa fa') (hom A a (u fa')) + ( first (iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( to-left-adjoint-components-is-rezk-is-segal) + ( ηa-transposition fa') + ( iso-eq-iso-is-rezk-application)) + +#def compute-covariant-transport-of-substitution-application + : covariant-transport B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa) = + covariant-transport A (u fa) (u fa') + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) + ( ηa) + := + compute-covariant-transport-of-substitution A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u + ( fa) ( fa') + ( to-left-adjoint-components-is-rezk-is-segal) + ( ηa) + +#def compute-covariant-transport-of-hom-family-is-segal-application + : covariant-transport A (u fa) (u fa') + ( to-left-adjoint-components-is-rezk-is-segal) + ( hom A a) (is-covariant-representable-is-segal A is-segal-A a) ηa = + comp-is-segal A is-segal-A a (u fa) (u fa') ηa + ( to-left-adjoint-components-is-rezk-is-segal) + := + compute-covariant-transport-of-hom-family-is-segal A is-segal-A + ( a) (u fa) (u fa') ( ηa) + ( to-left-adjoint-components-is-rezk-is-segal) + + +#def lem-10-8-application uses (extext a ηa ηa' ω ω') + : ( ap-hom B A u fa fa' (first (iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal)))) = + ( first ( iso-eq A is-segal-A (u fa) (u fa') (ap B A fa fa' u all-left-adjoint-components-equal-is-rezk-is-segal))) + := + compute-ap-hom-of-iso-eq B A (first is-rezk-B) is-segal-A u fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) + #end all-unit-arrows-equal-is-rezk-is-segal ``` From 564c8850a5c662762b298c3b11f696eb08e603d7 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sat, 21 Oct 2023 11:57:10 -0400 Subject: [PATCH 4/7] fixed bugs --- src/simplicial-hott/11-adjunctions.rzk.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index f39354e2..ed2f64b6 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -1680,7 +1680,7 @@ of `#!rzk is-transposing-right-adj A B u` ( ηa-transposition fa') ( iso-eq-iso-is-rezk-application)) -#def compute-covariant-transport-of-substitution-application +#def compute-covariant-transport-of-substitution-application uses (ηa' ω) : covariant-transport B fa fa' ( to-left-adjoint-components-is-rezk-is-segal) ( \ b → hom A a (u b)) @@ -1699,16 +1699,17 @@ of `#!rzk is-transposing-right-adj A B u` ( to-left-adjoint-components-is-rezk-is-segal) ( ηa) -#def compute-covariant-transport-of-hom-family-is-segal-application +#def compute-covariant-transport-of-hom-family-is-segal-application uses (ηa' ω) : covariant-transport A (u fa) (u fa') - ( to-left-adjoint-components-is-rezk-is-segal) - ( hom A a) (is-covariant-representable-is-segal A is-segal-A a) ηa = + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( hom A a) (is-covariant-representable-is-segal A is-segal-A a) + ( ηa) = comp-is-segal A is-segal-A a (u fa) (u fa') ηa - ( to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) := compute-covariant-transport-of-hom-family-is-segal A is-segal-A ( a) (u fa) (u fa') ( ηa) - ( to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) #def lem-10-8-application uses (extext a ηa ηa' ω ω') From 94c8f99fe501d3373535fde24fae0cd54d17afdb Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sat, 21 Oct 2023 19:54:09 -0400 Subject: [PATCH 5/7] finished proof constructing an identification between unit components --- src/simplicial-hott/11-adjunctions.rzk.md | 129 ++++++++-------------- 1 file changed, 47 insertions(+), 82 deletions(-) diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index ed2f64b6..aecf1247 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -1600,40 +1600,7 @@ of `#!rzk is-transposing-right-adj A B u` ( from-left-adjoint-components-is-rezk-is-segal, eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) -#def rev-lem-10-7-application uses (extext ηa' ω ω') - : transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = - covariant-transport B fa fa' - ( first - ( iso-eq B (first is-rezk-B) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal))) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa) - := - rev (hom A a (u fa')) - ( covariant-transport B fa fa' - ( first - ( iso-eq B (first is-rezk-B) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal))) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa)) - ( transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) - ( compute-covariant-transport-of-hom-family-iso-eq-is-segal B - ( first is-rezk-B) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( fa) - ( fa') - ( all-left-adjoint-components-equal-is-rezk-is-segal) - ( ηa)) - -#def iso-eq-iso-is-rezk-application uses (extext A is-segal-A u a ηa ηa' ω ω') +#def iso-eq-iso-to-left-adjoint-components-is-rezk uses (extext A is-segal-A u a ηa ηa' ω ω') : first (iso-eq B (first is-rezk-B) fa fa' ( all-left-adjoint-components-equal-is-rezk-is-segal)) = to-left-adjoint-components-is-rezk-is-segal @@ -1645,17 +1612,11 @@ of `#!rzk is-transposing-right-adj A B u` ( from-left-adjoint-components-is-rezk-is-segal, eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) -#def rev-lem-10-7-application' uses (extext ηa' ω ω') +#def compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal uses (extext ηa' ω ω') : transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = - covariant-transport B fa fa' - ( to-left-adjoint-components-is-rezk-is-segal) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa) + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = ηa' := - concat (hom A a (u fa')) + quintuple-concat (hom A a (u fa')) ( transport B ( \ b → hom A a (u b)) fa fa' ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) ( covariant-transport B fa fa' @@ -1672,53 +1633,57 @@ of `#!rzk is-transposing-right-adj A B u` ( is-covariant-substitution-is-covariant A B (hom A a) ( is-covariant-representable-is-segal A is-segal-A a) u) ( ηa)) - ( rev-lem-10-7-application) + ( covariant-transport A (u fa) (u fa') + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) + ( ηa)) + ( comp-is-segal A is-segal-A a (u fa) (u fa') ηa + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( ( ηa')) + ( rev (hom A a (u fa')) + ( covariant-transport B fa fa' + ( first + ( iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + ( compute-covariant-transport-of-hom-family-iso-eq-is-segal B + ( first is-rezk-B) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( fa) + ( fa') + ( all-left-adjoint-components-equal-is-rezk-is-segal) + ( ηa))) ( ap (hom B fa fa') (hom A a (u fa')) ( first (iso-eq B (first is-rezk-B) fa fa' ( all-left-adjoint-components-equal-is-rezk-is-segal))) ( to-left-adjoint-components-is-rezk-is-segal) ( ηa-transposition fa') - ( iso-eq-iso-is-rezk-application)) - -#def compute-covariant-transport-of-substitution-application uses (ηa' ω) - : covariant-transport B fa fa' - ( to-left-adjoint-components-is-rezk-is-segal) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa) = - covariant-transport A (u fa) (u fa') - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) - ( hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) - ( ηa) - := - compute-covariant-transport-of-substitution A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u - ( fa) ( fa') - ( to-left-adjoint-components-is-rezk-is-segal) - ( ηa) - -#def compute-covariant-transport-of-hom-family-is-segal-application uses (ηa' ω) - : covariant-transport A (u fa) (u fa') - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) - ( hom A a) (is-covariant-representable-is-segal A is-segal-A a) - ( ηa) = - comp-is-segal A is-segal-A a (u fa) (u fa') ηa - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) - := - compute-covariant-transport-of-hom-family-is-segal A is-segal-A - ( a) (u fa) (u fa') ( ηa) - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) - + ( iso-eq-iso-to-left-adjoint-components-is-rezk)) + ( compute-covariant-transport-of-hom-family-is-segal A is-segal-A + ( a) (u fa) (u fa') ( ηa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( compute-covariant-transport-of-substitution A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u + ( fa) ( fa') + ( to-left-adjoint-components-is-rezk-is-segal) + ( ηa)) + ( triangle-to-left-adjoint-components-is-rezk-is-segal) -#def lem-10-8-application uses (extext a ηa ηa' ω ω') - : ( ap-hom B A u fa fa' (first (iso-eq B (first is-rezk-B) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal)))) = - ( first ( iso-eq A is-segal-A (u fa) (u fa') (ap B A fa fa' u all-left-adjoint-components-equal-is-rezk-is-segal))) +#def all-unit-components-equal-is-rezk-is-segal uses (extext A is-segal-A u a ω ω') + : (fa, ηa) =_{Σ (b : B), hom A a (u b)} (fa', ηa') := - compute-ap-hom-of-iso-eq B A (first is-rezk-B) is-segal-A u fa fa' + path-of-pairs-pair-of-paths B (\ b → hom A a (u b)) ( fa) ( fa') ( all-left-adjoint-components-equal-is-rezk-is-segal) + ( ηa) ( ηa') + compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal #end all-unit-arrows-equal-is-rezk-is-segal ``` From bbb604f003ba87dd36af63ac779fd3c646a570bc Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sun, 22 Oct 2023 16:29:54 -0400 Subject: [PATCH 6/7] conversion to new style conventions? --- src/simplicial-hott/11-adjunctions.rzk.md | 1748 +++++++++------------ 1 file changed, 751 insertions(+), 997 deletions(-) diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index aecf1247..49079766 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -65,9 +65,9 @@ transformations, and a pair of witnesses to the triangle identities. ( u : B → A) : U := - Σ (η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)), - Σ (ϵ : nat-trans B (\ _ → B) (comp B A B f u) (identity B)), - product + Σ ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , Σ ( ϵ : nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + , product ( hom2 (B → A) u (triple-comp B A B A u f u) u ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) @@ -178,8 +178,8 @@ boundary data of a 3-simplex in lexicographic order. ( α₀ : hom2 A x y z g h hg) : U := - ( ((t₁ , t₂ ) , t₃ ) : Δ³) → - A [ t₃ ≡ 0₂ ↦ α₃ (t₁ , t₂ ), + ( ((t₁ , t₂ ) , t₃ ) : Δ³) + → A [ t₃ ≡ 0₂ ↦ α₃ (t₁ , t₂ ), t₂ ≡ t₃ ↦ α₂ (t₁ , t₃ ), t₁ ≡ t₂ ↦ α₁ (t₁ , t₃ ), t₁ ≡ 1₂ ↦ α₀ (t₂ , t₃ )] @@ -192,9 +192,8 @@ boundary data of a 3-simplex in lexicographic order. ( u : B → A) : U := - Σ ( (η , (ϵ , (α , β))) : has-quasi-diagrammatic-adj A B f u), - Σ ( μ : hom2 - ( B → B) + Σ ( (η , (ϵ , (α , β))) : has-quasi-diagrammatic-adj A B f u) + , Σ ( μ : hom2 ( B → B) ( comp B A B f u) ( quadruple-comp B A B A B f u f u) ( identity B) @@ -202,57 +201,49 @@ boundary data of a 3-simplex in lexicographic order. ( horizontal-comp-nat-trans B B B ( comp B A B f u) (identity B) (comp B A B f u) (identity B) ( ϵ) ( ϵ)) - ( ϵ)), - product - ( hom3 (B → B) - ( comp B A B f u) - ( quadruple-comp B A B A B f u f u) - ( comp B A B f u) - ( identity B) - ( whisker-nat-trans B A A B u (identity A) (comp A B A u f) f η) - ( id-hom (B → B) (comp B A B f u)) - ( ϵ) - ( postwhisker-nat-trans B B B - ( comp B A B f u) (identity B) (comp B A B f u) ϵ) - ( horizontal-comp-nat-trans B B B - ( comp B A B f u) (identity B) (comp B A B f u) (identity B) - ( ϵ) ( ϵ)) - ( ϵ) - ( \ t a → f (α t a)) - ( μ) - ( id-comp-witness (B → B) (comp B A B f u) (identity B) ϵ) - ( left-gray-interchanger-horizontal-comp-nat-trans B B B - ( comp B A B f u) (identity B) ( comp B A B f u) (identity B) + ( ϵ)) + , product + ( hom3 (B → B) + ( comp B A B f u) + ( quadruple-comp B A B A B f u f u) + ( comp B A B f u) + ( identity B) + ( whisker-nat-trans B A A B u (identity A) (comp A B A u f) f η) + ( id-hom (B → B) (comp B A B f u)) ( ϵ) - ( ϵ))) - ( hom3 - ( B → B) - ( comp B A B f u) - ( quadruple-comp B A B A B f u f u) - ( comp B A B f u) - ( identity B) - ( whisker-nat-trans B A A B u (identity A) (comp A B A u f) f η) - ( id-hom (B → B) (comp B A B f u)) - ( ϵ) - ( prewhisker-nat-trans B B B - ( comp B A B f u) (comp B A B f u) (identity B) ϵ) - ( horizontal-comp-nat-trans B B B - ( comp B A B f u) (identity B) (comp B A B f u) (identity B) - ( ϵ) ( ϵ)) - ( ϵ) - ( \ t b → β t (u b)) - ( μ) - ( id-comp-witness (B → B) (comp B A B f u) (identity B) ϵ) - ( right-gray-interchanger-horizontal-comp-nat-trans B B B - ( comp B A B f u) (identity B) ( comp B A B f u) (identity B) + ( postwhisker-nat-trans B B B + ( comp B A B f u) (identity B) (comp B A B f u) ϵ) + ( horizontal-comp-nat-trans B B B + ( comp B A B f u) (identity B) (comp B A B f u) (identity B) (ϵ) (ϵ)) ( ϵ) - ( ϵ))) + ( \ t a → f (α t a)) + ( μ) + ( id-comp-witness (B → B) (comp B A B f u) (identity B) ϵ) + ( left-gray-interchanger-horizontal-comp-nat-trans B B B + ( comp B A B f u) (identity B) (comp B A B f u) (identity B) (ϵ) (ϵ))) + ( hom3 (B → B) + ( comp B A B f u) + ( quadruple-comp B A B A B f u f u) + ( comp B A B f u) + ( identity B) + ( whisker-nat-trans B A A B u (identity A) (comp A B A u f) f η) + ( id-hom (B → B) (comp B A B f u)) + ( ϵ) + ( prewhisker-nat-trans B B B + ( comp B A B f u) (comp B A B f u) (identity B) ϵ) + ( horizontal-comp-nat-trans B B B + ( comp B A B f u) (identity B) (comp B A B f u) (identity B) (ϵ) (ϵ)) + ( ϵ) + ( \ t b → β t (u b)) + ( μ) + ( id-comp-witness (B → B) (comp B A B f u) (identity B) ϵ) + ( right-gray-interchanger-horizontal-comp-nat-trans B B B + ( comp B A B f u) (identity B) (comp B A B f u) (identity B) (ϵ) (ϵ))) #def half-adjoint-diagrammatic-adj ( A B : U) : U := Σ (f : A → B), Σ (u : B → A), is-half-adjoint-diagrammatic-adj A B f u - ``` ## Bi-diagrammatic adjunction @@ -269,18 +260,18 @@ triangle identities, one involving each counit. ( u : B → A) : U := - Σ (η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)), - Σ (ϵ : nat-trans B (\ _ → B) (comp B A B f u) (identity B)), - Σ (ϵ' : nat-trans B (\ _ → B) (comp B A B f u) (identity B)), - product - ( hom2 (B → A) u (triple-comp B A B A u f u) u - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) - ( id-hom (B → A) u)) - ( hom2 (A → B) f (triple-comp A B A B f u f) f - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ' ) - ( id-hom (A → B) f)) + Σ (η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , Σ (ϵ : nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + , Σ (ϵ' : nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + , product + ( hom2 (B → A) u (triple-comp B A B A u f u) u + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + ( id-hom (B → A) u)) + ( hom2 (A → B) f (triple-comp A B A B f u f) f + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ' ) + ( id-hom (A → B) f)) #def bi-diagrammatic-adj (A B : U) @@ -312,9 +303,11 @@ where "quasi-equivalence" is another name for "invertible map." ( f : A → B) ( u : B → A) : U - := (a : A) → (b : B) → - Σ (ϕ : (hom B (f a) b) → (hom A a (u b))), - has-inverse (hom B (f a) b) (hom A a (u b)) ϕ + := + (a : A) + → ( b : B) + → Σ ( ϕ : (hom B (f a) b) → (hom A a (u b))) + , has-inverse (hom B (f a) b) (hom A a (u b)) ϕ #def quasi-transposing-adj ( A B : U) @@ -355,50 +348,42 @@ in the usual way, as an application of the Yoneda lemma. (a : A) : Equiv ((b : B) → (hom B (f a) b) → (hom A a (u b))) (hom A a (u (f a))) := - ( evid B (f a) (\ b → hom A a (u b)) , - yoneda-lemma - ( funext) - ( B) - ( is-segal-B) - ( f a) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant - ( A) - ( B) - ( hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) - ( u))) + ( evid B (f a) (\ b → hom A a (u b)) + , + yoneda-lemma funext B is-segal-B + ( f a) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B + ( hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) + ( u))) #def equiv-unit-components : Equiv ( (a : A) → hom A a (u (f a))) ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) := - inv-equiv - ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) - ( (a : A) → hom A a (u (f a))) - ( equiv-components-nat-trans - ( A) - ( \ _ → A) - ( identity A) - ( comp A B A u f)) + inv-equiv + ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( (a : A) → hom A a (u (f a))) + ( equiv-components-nat-trans A ( \ _ → A) + ( identity A) + ( comp A B A u f)) #def equiv-transposition-unit uses (is-segal-A is-segal-B funext) : Equiv ( (a : A) → (b : B) → (hom B (f a) b) → (hom A a (u b))) ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) := - equiv-comp - ( (a : A) → (b : B) → (hom B (f a) b) → (hom A a (u b))) - ( (a : A) → hom A a (u (f a))) - ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) - ( equiv-function-equiv-family - ( funext) - ( A) - ( \ a → (b : B) → (hom B (f a) b) → (hom A a (u b))) - ( \ a → hom A a (u (f a))) - ( equiv-transposition-unit-component)) - ( equiv-unit-components) + equiv-comp + ( (a : A) → (b : B) → (hom B (f a) b) → (hom A a (u b))) + ( (a : A) → hom A a (u (f a))) + ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( equiv-function-equiv-family funext A + ( \ a → (b : B) → (hom B (f a) b) → (hom A a (u b))) + ( \ a → hom A a (u (f a))) + ( equiv-transposition-unit-component)) + ( equiv-unit-components) ``` We now reverse direction of the equivalence and extract the explicit map @@ -411,18 +396,13 @@ defining the transposition function associated to a unit natural transformation. ( \ ηa b k → comp-is-segal A is-segal-A a (u (f a)) (u b) ηa (ap-hom B A u (f a) b k)) := - inv-yoneda-lemma - ( funext) - ( B) - ( is-segal-B) - ( f a) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant - ( A) - ( B) - ( hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) - ( u)) + inv-yoneda-lemma funext B is-segal-B + ( f a) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B + ( hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) + ( u)) #def is-equiv-unit-transposition uses (is-segal-A is-segal-B funext) : is-equiv @@ -433,26 +413,24 @@ defining the transposition function associated to a unit natural transformation. ( \ t -> η t a) ( ap-hom B A u (f a) b k)) := - is-equiv-comp - ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) - ( (a : A) → hom A a (u (f a))) - ( (a : A) → (b : B) → (hom B (f a) b) → (hom A a (u b))) - ( ev-components-nat-trans A (\ _ → A) (identity A) (comp A B A u f)) - ( is-equiv-ev-components-nat-trans A (\ _ → A)(identity A)(comp A B A u f)) - ( \ η a b k → + is-equiv-comp + ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( (a : A) → hom A a (u (f a))) + ( (a : A) → (b : B) → (hom B (f a) b) → (hom A a (u b))) + ( ev-components-nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( is-equiv-ev-components-nat-trans A (\ _ → A)(identity A)(comp A B A u f)) + ( \ η a b k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( η a) + ( ap-hom B A u (f a) b k)) + ( is-equiv-function-is-equiv-family funext A + ( \ a → hom A a (u (f a))) + ( \ a → (b : B) → (hom B (f a) b) → (hom A a (u b))) + ( \ a ηa b k → comp-is-segal A is-segal-A a (u (f a)) (u b) - ( \ t -> η a t) + ( ηa) ( ap-hom B A u (f a) b k)) - ( is-equiv-function-is-equiv-family - ( funext) - ( A) - ( \ a → hom A a (u (f a))) - ( \ a → (b : B) → (hom B (f a) b) → (hom A a (u b))) - ( \ a ηa b k → - comp-is-segal A is-segal-A a (u (f a)) (u b) - ( ηa) - ( ap-hom B A u (f a) b k)) - ( is-equiv-unit-component-transposition)) + ( is-equiv-unit-component-transposition)) ``` The results for counits are dual. @@ -462,50 +440,42 @@ The results for counits are dual. (b : B) : Equiv ((a : A) → (hom A a (u b)) → (hom B (f a) b)) (hom B (f (u b)) b) := - ( contra-evid A (u b) (\ a → hom B (f a) b) , - contra-yoneda-lemma - ( funext) - ( A) - ( is-segal-A) - ( u b) - ( \ a → hom B (f a) b) - ( is-contravariant-substitution-is-contravariant - ( B) - ( A) - ( \ x -> hom B x b) - ( is-contravariant-representable-is-segal B is-segal-B b) - ( f))) + ( contra-evid A (u b) (\ a → hom B (f a) b) + , + contra-yoneda-lemma funext A is-segal-A + ( u b) + ( \ a → hom B (f a) b) + ( is-contravariant-substitution-is-contravariant B A + ( \ x -> hom B x b) + ( is-contravariant-representable-is-segal B is-segal-B b) + ( f))) #def equiv-counit-components : Equiv ( (b : B) → hom B (f (u b)) b) ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) := - inv-equiv - ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) - ( (b : B) → hom B (f (u b)) b) - ( equiv-components-nat-trans - ( B) - ( \ _ → B) - ( comp B A B f u) - ( identity B)) + inv-equiv + ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + ( (b : B) → hom B (f (u b)) b) + ( equiv-components-nat-trans B ( \ _ → B) + ( comp B A B f u) + ( identity B)) #def equiv-transposition-counit uses (is-segal-A is-segal-B funext) : Equiv ( (b : B) → (a : A) → (hom A a (u b)) → (hom B (f a) b)) ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) := - equiv-comp - ( (b : B) → (a : A) → (hom A a (u b)) → (hom B (f a) b)) - ( (b : B) → hom B (f (u b)) b) - ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) - ( equiv-function-equiv-family - ( funext) - ( B) - ( \ b → (a : A) → (hom A a (u b)) → (hom B (f a) b)) - ( \ b → hom B (f (u b)) b) - ( equiv-transposition-counit-component)) - ( equiv-counit-components) + equiv-comp + ( (b : B) → (a : A) → (hom A a (u b)) → (hom B (f a) b)) + ( (b : B) → hom B (f (u b)) b) + ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + ( equiv-function-equiv-family funext B + ( \ b → (a : A) → (hom A a (u b)) → (hom B (f a) b)) + ( \ b → hom B (f (u b)) b) + ( equiv-transposition-counit-component)) + ( equiv-counit-components) ``` We again reverse direction of the equivalence and extract the explicit map @@ -515,22 +485,18 @@ transformation. ```rzk #def is-equiv-counit-component-transposition uses (funext) (b : B) - : is-equiv (hom B (f (u b)) b) ((a : A) → (hom A a (u b)) → (hom B (f a) b)) + : is-equiv (hom B (f (u b)) b) + ( (a : A) → (hom A a (u b)) → (hom B (f a) b)) ( \ ϵb a k → comp-is-segal B is-segal-B (f a) (f (u b)) b (ap-hom A B f a (u b) k) ϵb) := - inv-contra-yoneda-lemma - ( funext) - ( A) - ( is-segal-A) - ( u b) - ( \ a → hom B (f a) b) - ( is-contravariant-substitution-is-contravariant - ( B) - ( A) - ( \ z → hom B z b) - ( is-contravariant-representable-is-segal B is-segal-B b) - ( f)) + inv-contra-yoneda-lemma funext A is-segal-A + ( u b) + ( \ a → hom B (f a) b) + ( is-contravariant-substitution-is-contravariant B A + ( \ z → hom B z b) + ( is-contravariant-representable-is-segal B is-segal-B b) + ( f)) #def is-equiv-counit-transposition uses (is-segal-A is-segal-B funext) : is-equiv @@ -541,26 +507,24 @@ transformation. ( ap-hom A B f a (u b) k) ( \ t -> ϵ t b)) := - is-equiv-comp - ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) - ( (b : B) → hom B (f (u b)) b) - ( (b : B) → (a : A) → (hom A a (u b)) → (hom B (f a) b)) - ( ev-components-nat-trans B (\ _ → B) (comp B A B f u) (identity B)) - ( is-equiv-ev-components-nat-trans B (\ _ → B)(comp B A B f u) (identity B)) - ( \ ϵ b a k → + is-equiv-comp + ( nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + ( (b : B) → hom B (f (u b)) b) + ( (b : B) → (a : A) → (hom A a (u b)) → (hom B (f a) b)) + ( ev-components-nat-trans B (\ _ → B) (comp B A B f u) (identity B)) + ( is-equiv-ev-components-nat-trans B (\ _ → B)(comp B A B f u) (identity B)) + ( \ ϵ b a k → + comp-is-segal B is-segal-B (f a) (f (u b)) b + ( ap-hom A B f a (u b) k) + ( ϵ b)) + ( is-equiv-function-is-equiv-family funext B + ( \ b → hom B (f (u b)) b) + ( \ b → (a : A) → (hom A a (u b)) → (hom B (f a) b)) + ( \ b ϵb a k → comp-is-segal B is-segal-B (f a) (f (u b)) b ( ap-hom A B f a (u b) k) - ( \ t -> ϵ b t)) - ( is-equiv-function-is-equiv-family - ( funext) - ( B) - ( \ b → hom B (f (u b)) b) - ( \ b → (a : A) → (hom A a (u b)) → (hom B (f a) b)) - ( \ b ϵb a k → - comp-is-segal B is-segal-B (f a) (f (u b)) b - ( ap-hom A B f a (u b) k) - ( ϵb)) - ( is-equiv-counit-component-transposition)) + ( ϵb)) + ( is-equiv-counit-component-transposition)) #end unit-counit-transposition ``` @@ -596,40 +560,29 @@ as an application of the dependent Yoneda lemma. (triple-comp B A B A u f u) ( u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + = ( id-hom (B → A) u)) := - inv-equiv - ( ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = - ( id-hom (B → A) u)) - ( hom2 (B → A) u (triple-comp B A B A u f u) u - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) - ( id-hom (B → A) u)) - ( equiv-hom2-eq-comp-is-segal + inv-equiv + ( ( comp-is-segal ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) - ( id-hom (B → A) u)) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = + ( id-hom (B → A) u)) + ( hom2 (B → A) u (triple-comp B A B A u f u) u + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + ( id-hom (B → A) u)) + ( equiv-hom2-eq-comp-is-segal + ( B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + ( id-hom (B → A) u)) #def equiv-ev-components-radj-triangle : Equiv @@ -644,7 +597,8 @@ as an application of the dependent Yoneda lemma. (triple-comp B A B A u f u) ( u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + = ( id-hom (B → A) u)) ( ( ev-components-nat-trans B (\ _ → A) u u ( comp-is-segal @@ -658,246 +612,172 @@ as an application of the dependent Yoneda lemma. (triple-comp B A B A u f u) ( u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) = + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) + = ( \ b → id-hom A ( u b))) := - equiv-ap-is-equiv - ( nat-trans B (\ _ → A) u u) - ( nat-trans-components B (\ _ → A) u u) - ( ev-components-nat-trans B (\ _ → A) u u) - ( is-equiv-ev-components-nat-trans B (\ _ → A) u u) - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( id-hom (B → A) u) + equiv-ap-is-equiv + ( nat-trans B (\ _ → A) u u) + ( nat-trans-components B (\ _ → A) u u) + ( ev-components-nat-trans B (\ _ → A) u u) + ( is-equiv-ev-components-nat-trans B (\ _ → A) u u) + ( comp-is-segal (B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + ( id-hom (B → A) u) #def equiv-components-radj-triangle-funext uses (funext) : Equiv - ( ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) = + ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type funext B (\ _ → A) (\ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + = ( \ b → id-hom A ( u b))) ( ( b : B) → - ( ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) = - ( id-hom A ( u b)))) + ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type funext B (\ _ → A) (\ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + ( b) + = + id-hom A ( u b))) := - equiv-FunExt - ( funext) - ( B) - ( \ b → (hom A (u b) (u b))) - ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) - ( \ b → id-hom A (u b)) + equiv-FunExt funext B + ( \ b → (hom A (u b) (u b))) + ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type funext B (\ _ → A) (\ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) + ( \ b → id-hom A (u b)) #def eq-ladj-triangle-comp-components-comp-nat-trans-is-segal uses (funext) (b : B) - : ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = - ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type (funext) (B) (\ _ → A) (\ _ → is-segal-A)) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) - := - comp-components-comp-nat-trans-is-segal - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + : comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b)) + = + ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type (funext) (B) (\ _ → A) (\ _ → is-segal-A)) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) ( b) + := + comp-components-comp-nat-trans-is-segal funext B (\ _ → A) (\ _ → is-segal-A) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + ( b) #def equiv-preconcat-radj-triangle uses (funext) (b : B) : Equiv - ( ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) = - ( id-hom A ( u b))) - ( ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = - ( id-hom A ( u b))) - := - equiv-preconcat - ( hom A (u b) (u b)) - ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type (funext) (B) (\ _ → A) (\ _ → is-segal-A)) - ( u) - (triple-comp B A B A u f u) - ( u) + ( comp-is-segal (B → A) + ( is-segal-function-type funext B (\ _ → A) (\ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) - ( id-hom A (u b)) - (eq-ladj-triangle-comp-components-comp-nat-trans-is-segal b) + ( b) + = + id-hom A ( u b)) + ( ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + = + ( id-hom A ( u b))) + := + equiv-preconcat ( hom A (u b) (u b)) + ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type (funext) (B) (\ _ → A) (\ _ → is-segal-A)) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + ( b)) + ( id-hom A (u b)) + ( eq-ladj-triangle-comp-components-comp-nat-trans-is-segal b) #def equiv-component-comp-segal-comp-radj-triangle uses (funext) : Equiv - ( ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = - ( id-hom (B → A) u)) + ( comp-is-segal ( B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + = + id-hom (B → A) u) ( ( b : B) → ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + = ( id-hom A ( u b))) := - equiv-triple-comp - ( ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) + equiv-triple-comp + ( ( comp-is-segal (B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = + ( id-hom (B → A) u)) + ( ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal (B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = - ( id-hom (B → A) u)) - ( ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) = - ( \ b → id-hom A ( u b))) - ( ( b : B) → - ( ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ))) + = + ( \ b → id-hom A ( u b))) + ( ( b : B) + → ( ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal ( B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) = + ( b)) + = ( id-hom A ( u b)))) - ( ( b : B) → + ( ( b : B) + → ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + = + ( id-hom A ( u b))) + ( equiv-ev-components-radj-triangle) + ( equiv-components-radj-triangle-funext) + ( equiv-function-equiv-family funext B + ( \ b → + ( ev-components-nat-trans B (\ _ → A) u u + ( comp-is-segal ( B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + ( b)) + = + ( id-hom A ( u b))) + ( \ b → ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + = ( id-hom A ( u b))) - ( equiv-ev-components-radj-triangle) - ( equiv-components-radj-triangle-funext) - ( equiv-function-equiv-family - ( funext) - ( B) - ( \ b → - ( ev-components-nat-trans B (\ _ → A) u u - ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) - ( b)) = - ( id-hom A ( u b))) - ( \ b → - ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = - ( id-hom A ( u b))) - ( equiv-preconcat-radj-triangle)) + ( equiv-preconcat-radj-triangle)) ``` We finally arrive at the desired equivalence. @@ -909,37 +789,32 @@ We finally arrive at the desired equivalence. ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) ( id-hom (B → A) u)) - ( ( b : B) → - ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = - ( id-hom A ( u b))) + ( ( b : B) + → ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = + ( id-hom A ( u b))) := - equiv-comp - ( hom2 (B → A) u (triple-comp B A B A u f u) u + equiv-comp + ( hom2 (B → A) u (triple-comp B A B A u f u) u + ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) + ( id-hom (B → A) u)) + ( ( comp-is-segal ( B → A) + ( is-segal-function-type funext B ( \ _ → A) ( \ _ → is-segal-A )) + ( u) (triple-comp B A B A u f u) (u) ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ ) - ( id-hom (B → A) u)) - ( ( comp-is-segal - ( B → A) - ( is-segal-function-type - ( funext) - ( B) - ( \ _ → A) - ( \ _ → is-segal-A )) - ( u) - (triple-comp B A B A u f u) - ( u) - ( prewhisker-nat-trans B A A u (identity A) (comp A B A u f) η ) - ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) = - ( id-hom (B → A) u)) - ( ( b : B) → - ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) - ( \ t → η t (u b) ) - ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) = + ( postwhisker-nat-trans B B A (comp B A B f u) (identity B) u ϵ )) + = + ( id-hom (B → A) u)) + ( ( b : B) + → ( comp-is-segal A is-segal-A (u b) (u (f (u b))) (u b) + ( \ t → η t (u b) ) + ( ap-hom B A u (f (u b)) b (\ t → ϵ t b))) + = ( id-hom A ( u b))) - ( equiv-radj-triangle) - ( equiv-component-comp-segal-comp-radj-triangle) + ( equiv-radj-triangle) + ( equiv-component-comp-segal-comp-radj-triangle) ``` The calculation for the other triangle identity is dual. @@ -948,155 +823,96 @@ The calculation for the other triangle identity is dual. #def equiv-ladj-triangle uses (funext) : Equiv ( hom2 (A → B) f (triple-comp A B A B f u f) f - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) - ( id-hom (A → B) f)) - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ a → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - := - inv-equiv - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - ( hom2 (A → B) f (triple-comp A B A B f u f) f - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) - ( id-hom (A → B) f)) - ( equiv-hom2-eq-comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) ( id-hom (A → B) f)) + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + := + inv-equiv + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + ( hom2 (A → B) f (triple-comp A B A B f u f) f + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + ( id-hom (A → B) f)) + ( equiv-hom2-eq-comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + ( id-hom (A → B) f)) #def equiv-ev-components-ladj-triangle : Equiv - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) = + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + = ( \ a → id-hom B ( f a))) := - equiv-ap-is-equiv - ( nat-trans A (\ _ → B) f f) - ( nat-trans-components A (\ _ → B) f f) - ( ev-components-nat-trans A (\ _ → B) f f) - ( is-equiv-ev-components-nat-trans A (\ _ → B) f f) - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( id-hom (A → B) f) + equiv-ap-is-equiv + ( nat-trans A (\ _ → B) f f) + ( nat-trans-components A (\ _ → B) f f) + ( ev-components-nat-trans A (\ _ → B) f f) + ( is-equiv-ev-components-nat-trans A (\ _ → B) f f) + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + ( id-hom (A → B) f) #def equiv-components-ladj-triangle-funext uses (funext) : Equiv - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) = + ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + = ( \ a → id-hom B ( f a))) - ( ( a : A) → - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) + ( ( a : A) + → ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( a)) = - ( id-hom B ( f a)))) + ( a) + = + id-hom B ( f a))) := - equiv-FunExt - ( funext) - ( A) - ( \ a → (hom B (f a) (f a))) - ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) - ( \ a → id-hom B (f a)) + equiv-FunExt funext A + ( \ a → (hom B (f a) (f a))) + ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) + ( \ a → id-hom B (f a)) #def eq-radj-triangle-comp-components-comp-nat-trans-is-segal uses (funext) (a : A) @@ -1129,144 +945,100 @@ The calculation for the other triangle identity is dual. #def equiv-preconcat-ladj-triangle uses (funext) (a : A) : Equiv - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( a)) = - ( id-hom B ( f a))) - ( ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) - ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) - := - equiv-preconcat - ( hom B (f a) (f a)) - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) - ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( a)) - ( id-hom B (f a)) - (eq-radj-triangle-comp-components-comp-nat-trans-is-segal a) + ( a) + = + id-hom B ( f a)) + ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( ap-hom A B f a (u (f a)) (\ t → η t a)) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) + := + equiv-preconcat (hom B (f a) (f a)) + ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( ap-hom A B f a (u (f a)) (\ t → η t a)) + ( \ t → ϵ t (f a))) + ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + ( a)) + ( id-hom B (f a)) + (eq-radj-triangle-comp-components-comp-nat-trans-is-segal a) #def equiv-component-comp-segal-comp-ladj-triangle uses (funext) : Equiv - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - ( ( a : A) → - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + ( ( a : A) + → comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) := - equiv-triple-comp - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) + equiv-triple-comp + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + ( ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) = - ( \ a → id-hom B ( f a))) - ( ( a : A) → - ( ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( a)) = - ( id-hom B ( f a)))) - ( ( a : A) → - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ))) + = + ( \ a → id-hom B ( f a))) + ( ( a : A) + → ( ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + ( a) + = + id-hom B ( f a))) + ( ( a : A) + → comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) ( equiv-ev-components-ladj-triangle) ( equiv-components-ladj-triangle-funext) - ( equiv-function-equiv-family - ( funext) - ( A) + ( equiv-function-equiv-family funext A ( \ a → - ( ev-components-nat-trans A (\ _ → B) f f - ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) - ( a)) = - ( id-hom B ( f a))) + ev-components-nat-trans A (\ _ → B) f f + ( comp-is-segal ( A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) + ( a) + = + id-hom B ( f a)) ( \ a → - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) ( equiv-preconcat-ladj-triangle)) #def equiv-components-ladj-triangle uses (funext) @@ -1275,37 +1047,33 @@ The calculation for the other triangle identity is dual. ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) ( id-hom (A → B) f)) - ( ( a : A) → - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( ( a : A) + → comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) := - equiv-comp - ( hom2 (A → B) f (triple-comp A B A B f u f) f - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) - ( id-hom (A → B) f)) - ( ( comp-is-segal - ( A → B) - ( is-segal-function-type - ( funext) - ( A) - ( \ _ → B) - ( \ _ → is-segal-B )) - ( f) - (triple-comp A B A B f u f) - ( f) - ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) - ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ )) = - ( id-hom (A → B) f)) - ( ( a : A) → - ( comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) - ( ap-hom A B f a (u (f a)) (\ t → η t a)) - ( \ t → ϵ t (f a))) = - ( id-hom B ( f a))) - ( equiv-ladj-triangle) - ( equiv-component-comp-segal-comp-ladj-triangle) + equiv-comp + ( hom2 (A → B) f (triple-comp A B A B f u f) f + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + ( id-hom (A → B) f)) + ( comp-is-segal (A → B) + ( is-segal-function-type funext A ( \ _ → B) ( \ _ → is-segal-B )) + ( f) (triple-comp A B A B f u f) (f) + ( postwhisker-nat-trans A A B (identity A) (comp A B A u f) f η ) + ( prewhisker-nat-trans A B B f (comp B A B f u) (identity B) ϵ ) + = + id-hom (A → B) f) + ( ( a : A) + → comp-is-segal B is-segal-B (f a) (f (u (f a))) (f a) + ( ap-hom A B f a (u (f a)) (\ t → η t a)) + ( \ t → ϵ t (f a)) + = + id-hom B ( f a)) + ( equiv-ladj-triangle) + ( equiv-component-comp-segal-comp-ladj-triangle) #end triangle-identities ``` @@ -1341,47 +1109,49 @@ of `#!rzk is-transposing-right-adj A B u` : (hom A a (u b)) := comp-is-segal A is-segal-A a (u fa') (u b) ηa' (ap-hom B A u fa' b k) -#variable ω : (b : B) → is-equiv (hom B fa b) (hom A a (u b)) (ηa-transposition b) +#variable ω + : (b : B) → is-equiv (hom B fa b) (hom A a (u b)) (ηa-transposition b) -#variable ω' : (b : B) → is-equiv (hom B fa' b) (hom A a (u b)) (ηa'-transposition b) +#variable ω' + : (b : B) → is-equiv (hom B fa' b) (hom A a (u b)) (ηa'-transposition b) #def to-left-adjoint-components-is-rezk-is-segal uses (A is-segal-A u a ηa) : hom B fa fa' := - ( section-is-equiv (hom B fa fa') (hom A a (u fa')) - ( ηa-transposition fa') (ω fa')) - ( ηa') + section-is-equiv (hom B fa fa') (hom A a (u fa')) + ( ηa-transposition fa') (ω fa') + ( ηa') #def triangle-to-left-adjoint-components-is-rezk-is-segal : comp-is-segal A is-segal-A a (u fa) (u fa') ( ηa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)) = - ( ηa') + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + = + ηa' := - ( second - ( has-section-is-equiv (hom B fa fa') (hom A a (u fa')) - ( ηa-transposition fa') (ω fa'))) - ( ηa') + ( second + ( has-section-is-equiv (hom B fa fa') (hom A a (u fa')) + ( ηa-transposition fa') (ω fa'))) + ( ηa') #def from-left-adjoint-components-is-rezk-is-segal uses (A is-segal-A u a ηa') : hom B fa' fa := - ( section-is-equiv (hom B fa' fa) (hom A a (u fa)) - ( ηa'-transposition fa) (ω' fa)) - ( ηa) + section-is-equiv (hom B fa' fa) (hom A a (u fa)) + ( ηa'-transposition fa) (ω' fa) + ( ηa) #def triangle-from-left-adjoint-components-is-rezk-is-segal : comp-is-segal A is-segal-A a (u fa') (u fa) ( ηa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)) = - ( ηa) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal) + = + ηa := - ( second - ( has-section-is-equiv (hom B fa' fa) (hom A a (u fa)) - ( ηa'-transposition fa) (ω' fa))) - ( ηa) + ( second + ( has-section-is-equiv (hom B fa' fa) (hom A a (u fa)) + ( ηa'-transposition fa) (ω' fa))) + ( ηa) #def ηa-automorphism uses (extext ω ω') : comp-is-segal A is-segal-A a (u fa) (u fa) @@ -1389,65 +1159,55 @@ of `#!rzk is-transposing-right-adj A B u` ( ap-hom B A u fa fa ( comp-is-segal B (first is-rezk-B) fa fa' fa ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal))) = ηa - := - quadruple-concat (hom A a (u fa)) - ( comp-is-segal A is-segal-A a (u fa) (u fa) - ( ηa) - ( ap-hom B A u fa fa - ( comp-is-segal B (first is-rezk-B) fa fa' fa - ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal)))) - ( comp-is-segal A is-segal-A a (u fa) (u fa) - ( ηa) - ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)))) - ( comp-is-segal A is-segal-A a (u fa') (u fa) - ( comp-is-segal A is-segal-A a (u fa) (u fa') - ( ηa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal))) - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal))) - ( comp-is-segal A is-segal-A a (u fa') (u fa) - ( ηa') - ( ap-hom B A u fa' fa ( from-left-adjoint-components-is-rezk-is-segal))) + = + ηa + := + quadruple-concat (hom A a (u fa)) + ( comp-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( ap-hom B A u fa fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa) (u fa) ( ηa) - ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) + ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( comp-is-segal A is-segal-A a (u fa) (u fa') ( ηa) - ( ap-hom B A u fa fa - ( comp-is-segal B (first is-rezk-B) fa fa' fa - ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal))) - ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal))) - ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A - ( u) fa fa' fa + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( comp-is-segal A is-segal-A a (u fa') (u fa) + ( ηa') + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( ηa) + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) + ( ηa) + ( ap-hom B A u fa fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa ( to-left-adjoint-components-is-rezk-is-segal) ( from-left-adjoint-components-is-rezk-is-segal))) - ( rev-associative-is-segal extext A is-segal-A a (u fa) (u fa') (u fa) + ( comp-is-segal A is-segal-A (u fa) (u fa') (u fa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A u fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal))) + ( rev-associative-is-segal extext A is-segal-A a (u fa) (u fa') (u fa) + ( ηa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa') (u fa) + ( comp-is-segal A is-segal-A a (u fa) (u fa') ( ηa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal))) - ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa') (u fa) - ( comp-is-segal A is-segal-A a (u fa) (u fa') - ( ηa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal))) - ( ηa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)) - ( triangle-to-left-adjoint-components-is-rezk-is-segal)) - ( triangle-from-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( ηa') + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal) + ( triangle-to-left-adjoint-components-is-rezk-is-segal)) + ( triangle-from-left-adjoint-components-is-rezk-is-segal) #def ηa'-automorphism uses (extext ω ω') : comp-is-segal A is-segal-A a (u fa') (u fa') @@ -1455,149 +1215,138 @@ of `#!rzk is-transposing-right-adj A B u` ( ap-hom B A u fa' fa' ( comp-is-segal B (first is-rezk-B) fa' fa fa' ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal))) = ηa' - := - quadruple-concat (hom A a (u fa')) - ( comp-is-segal A is-segal-A a (u fa') (u fa') - ( ηa') - ( ap-hom B A u fa' fa' - ( comp-is-segal B (first is-rezk-B) fa' fa fa' - ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal)))) - ( comp-is-segal A is-segal-A a (u fa') (u fa') - ( ηa') - ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)))) - ( comp-is-segal A is-segal-A a (u fa) (u fa') - ( comp-is-segal A is-segal-A a (u fa') (u fa) - ( ηa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal))) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal))) - ( comp-is-segal A is-segal-A a (u fa) (u fa') - ( ηa) - ( ap-hom B A u fa fa' ( to-left-adjoint-components-is-rezk-is-segal))) + = + ηa' + := + quadruple-concat (hom A a (u fa')) + ( comp-is-segal A is-segal-A a (u fa') (u fa') ( ηa') - ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') + ( ap-hom B A u fa' fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal)))) + ( comp-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal))) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( comp-is-segal A is-segal-A a (u fa') (u fa) ( ηa') - ( ap-hom B A u fa' fa' - ( comp-is-segal B (first is-rezk-B) fa' fa fa' - ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal))) - ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal))) - ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A - ( u) fa' fa fa' + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( comp-is-segal A is-segal-A a (u fa) (u fa') + ( ηa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( ηa') + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') + ( ηa') + ( ap-hom B A u fa' fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' ( from-left-adjoint-components-is-rezk-is-segal) ( to-left-adjoint-components-is-rezk-is-segal))) - ( rev-associative-is-segal extext A is-segal-A a - ( u fa') (u fa) (u fa') + ( comp-is-segal A is-segal-A (u fa') (u fa) (u fa') + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( rev-functors-pres-comp B A (first is-rezk-B) is-segal-A u fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal))) + ( rev-associative-is-segal extext A is-segal-A a ( u fa') (u fa) (u fa') + ( ηa') + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa) (u fa') + ( comp-is-segal A is-segal-A a (u fa') (u fa) ( ηa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal)) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal))) - ( postwhisker-homotopy-is-segal (A) (is-segal-A) (a) (u fa) (u fa') - ( comp-is-segal A is-segal-A a (u fa') (u fa) - ( ηa') - ( ap-hom B A u fa' fa - ( from-left-adjoint-components-is-rezk-is-segal))) - ( ηa) - ( ap-hom B A u fa fa' - ( to-left-adjoint-components-is-rezk-is-segal)) - ( triangle-from-left-adjoint-components-is-rezk-is-segal)) - ( triangle-to-left-adjoint-components-is-rezk-is-segal) + ( ap-hom B A u fa' fa from-left-adjoint-components-is-rezk-is-segal)) + ( ηa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( triangle-from-left-adjoint-components-is-rezk-is-segal)) + ( triangle-to-left-adjoint-components-is-rezk-is-segal) #def eq-id-from-to-left-adjoint-components-is-rezk-is-segal uses (extext ηa' ω ω') - : ( comp-is-segal B (first is-rezk-B) fa fa' fa - ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal)) = - ( id-hom B fa) + : comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal) + = + id-hom B fa := - inv-ap-is-emb - ( hom B fa fa) - ( hom A a (u fa)) + inv-ap-is-emb (hom B fa fa) (hom A a (u fa)) + ( ηa-transposition fa) + ( is-emb-is-equiv (hom B fa fa) (hom A a (u fa)) ( ηa-transposition fa) - ( is-emb-is-equiv - ( hom B fa fa) - ( hom A a (u fa)) - ( ηa-transposition fa) - ( ω fa)) - ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( ω fa)) + ( comp-is-segal B (first is-rezk-B) fa fa' fa + ( to-left-adjoint-components-is-rezk-is-segal) + ( from-left-adjoint-components-is-rezk-is-segal)) + ( id-hom B fa) + ( zig-zag-concat (hom A a (u fa)) + ( ηa-transposition fa + ( comp-is-segal B (first is-rezk-B) fa fa' fa ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal)) - ( id-hom B fa) - ( zig-zag-concat (hom A a (u fa)) - ( ηa-transposition fa - ( comp-is-segal B (first is-rezk-B) fa fa' fa - ( to-left-adjoint-components-is-rezk-is-segal) - ( from-left-adjoint-components-is-rezk-is-segal))) - ( ηa) + ( from-left-adjoint-components-is-rezk-is-segal))) + ( ηa) + ( ηa-transposition fa (id-hom B fa)) + ( ηa-automorphism) + ( concat (hom A a (u fa)) ( ηa-transposition fa (id-hom B fa)) - ( ηa-automorphism) - ( concat (hom A a (u fa)) - ( ηa-transposition fa (id-hom B fa)) - ( comp-is-segal A is-segal-A a (u fa) (u fa) ηa (id-hom A (u fa))) - ( ηa) - ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) ηa - ( ap-hom B A u fa fa (id-hom B fa)) - ( id-hom A (u fa)) - (functors-pres-id extext B A u fa)) - ( comp-id-is-segal A is-segal-A a (u fa) ηa))) + ( comp-is-segal A is-segal-A a (u fa) (u fa) ηa (id-hom A (u fa))) + ( ηa) + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa) (u fa) ηa + ( ap-hom B A u fa fa (id-hom B fa)) + ( id-hom A (u fa)) + (functors-pres-id extext B A u fa)) + ( comp-id-is-segal A is-segal-A a (u fa) ηa))) #def eq-id-to-from-left-adjoint-components-is-rezk-is-segal uses (extext ηa ω ω') - : ( comp-is-segal B (first is-rezk-B) fa' fa fa' - ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal)) = - ( id-hom B fa') + : comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal) + = + id-hom B fa' := - inv-ap-is-emb + inv-ap-is-emb (hom B fa' fa') (hom A a (u fa')) + ( ηa'-transposition fa') + ( is-emb-is-equiv ( hom B fa' fa') ( hom A a (u fa')) ( ηa'-transposition fa') - ( is-emb-is-equiv - ( hom B fa' fa') - ( hom A a (u fa')) - ( ηa'-transposition fa') - ( ω' fa')) - ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( ω' fa')) + ( comp-is-segal B (first is-rezk-B) fa' fa fa' + ( from-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal)) + ( id-hom B fa') + ( zig-zag-concat (hom A a (u fa')) + ( ηa'-transposition fa' + ( comp-is-segal B (first is-rezk-B) fa' fa fa' ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal)) - ( id-hom B fa') - ( zig-zag-concat (hom A a (u fa')) - ( ηa'-transposition fa' - ( comp-is-segal B (first is-rezk-B) fa' fa fa' - ( from-left-adjoint-components-is-rezk-is-segal) - ( to-left-adjoint-components-is-rezk-is-segal))) - ( ηa') + ( to-left-adjoint-components-is-rezk-is-segal))) + ( ηa') + ( ηa'-transposition fa' (id-hom B fa')) + ( ηa'-automorphism) + ( concat (hom A a (u fa')) ( ηa'-transposition fa' (id-hom B fa')) - ( ηa'-automorphism) - ( concat (hom A a (u fa')) - ( ηa'-transposition fa' (id-hom B fa')) - ( comp-is-segal A is-segal-A a (u fa') (u fa') ηa' (id-hom A (u fa'))) - ( ηa') - ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') ηa' - ( ap-hom B A u fa' fa' (id-hom B fa')) - ( id-hom A (u fa')) - (functors-pres-id extext B A u fa')) - ( comp-id-is-segal A is-segal-A a (u fa') ηa'))) + ( comp-is-segal A is-segal-A a (u fa') (u fa') ηa' (id-hom A (u fa'))) + ( ηa') + ( prewhisker-homotopy-is-segal A is-segal-A a (u fa') (u fa') ηa' + ( ap-hom B A u fa' fa' (id-hom B fa')) + ( id-hom A (u fa')) + (functors-pres-id extext B A u fa')) + ( comp-id-is-segal A is-segal-A a (u fa') ηa'))) #def all-left-adjoint-components-equal-is-rezk-is-segal uses (extext A is-segal-A u a ηa ηa' ω ω') : fa = fa' := - eq-iso-is-rezk B is-rezk-B fa fa' - ( to-left-adjoint-components-is-rezk-is-segal, - (( from-left-adjoint-components-is-rezk-is-segal, - eq-id-from-to-left-adjoint-components-is-rezk-is-segal), - ( from-left-adjoint-components-is-rezk-is-segal, + eq-iso-is-rezk B is-rezk-B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal + , + ( ( from-left-adjoint-components-is-rezk-is-segal + , + eq-id-from-to-left-adjoint-components-is-rezk-is-segal) + , + ( from-left-adjoint-components-is-rezk-is-segal + , eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) #def iso-eq-iso-to-left-adjoint-components-is-rezk uses (extext A is-segal-A u a ηa ηa' ω ω') @@ -1605,20 +1354,49 @@ of `#!rzk is-transposing-right-adj A B u` ( all-left-adjoint-components-equal-is-rezk-is-segal)) = to-left-adjoint-components-is-rezk-is-segal := - iso-eq-iso-is-rezk B is-rezk-B fa fa' - ( to-left-adjoint-components-is-rezk-is-segal, - ( ( from-left-adjoint-components-is-rezk-is-segal, - eq-id-from-to-left-adjoint-components-is-rezk-is-segal), - ( from-left-adjoint-components-is-rezk-is-segal, - eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) + iso-eq-iso-is-rezk B is-rezk-B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal + , + ( ( from-left-adjoint-components-is-rezk-is-segal + , + eq-id-from-to-left-adjoint-components-is-rezk-is-segal) + , + ( from-left-adjoint-components-is-rezk-is-segal + , + eq-id-to-from-left-adjoint-components-is-rezk-is-segal))) #def compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal uses (extext ηa' ω ω') : transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa = ηa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa + = + ηa' := - quintuple-concat (hom A a (u fa')) - ( transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + quintuple-concat (hom A a (u fa')) + ( transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + ( covariant-transport B fa fa' + ( first + ( iso-eq B (first is-rezk-B) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal))) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( covariant-transport B fa fa' + ( to-left-adjoint-components-is-rezk-is-segal) + ( \ b → hom A a (u b)) + ( is-covariant-substitution-is-covariant A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u) + ( ηa)) + ( covariant-transport A (u fa) (u fa') + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) + ( hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) + ( ηa)) + ( comp-is-segal A is-segal-A a (u fa) (u fa') ηa + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( ( ηa')) + ( rev (hom A a (u fa')) ( covariant-transport B fa fa' ( first ( iso-eq B (first is-rezk-B) fa fa' @@ -1627,63 +1405,39 @@ of `#!rzk is-transposing-right-adj A B u` ( is-covariant-substitution-is-covariant A B (hom A a) ( is-covariant-representable-is-segal A is-segal-A a) u) ( ηa)) - ( covariant-transport B fa fa' - ( to-left-adjoint-components-is-rezk-is-segal) + ( transport B ( \ b → hom A a (u b)) fa fa' + ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) + ( compute-covariant-transport-of-hom-family-iso-eq-is-segal B + ( first is-rezk-B) ( \ b → hom A a (u b)) ( is-covariant-substitution-is-covariant A B (hom A a) ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa)) - ( covariant-transport A (u fa) (u fa') - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal) - ( hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) - ( ηa)) - ( comp-is-segal A is-segal-A a (u fa) (u fa') ηa - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) - ( ( ηa')) - ( rev (hom A a (u fa')) - ( covariant-transport B fa fa' - ( first - ( iso-eq B (first is-rezk-B) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal))) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( ηa)) - ( transport B ( \ b → hom A a (u b)) fa fa' - ( all-left-adjoint-components-equal-is-rezk-is-segal) ηa) - ( compute-covariant-transport-of-hom-family-iso-eq-is-segal B - ( first is-rezk-B) - ( \ b → hom A a (u b)) - ( is-covariant-substitution-is-covariant A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u) - ( fa) - ( fa') - ( all-left-adjoint-components-equal-is-rezk-is-segal) - ( ηa))) - ( ap (hom B fa fa') (hom A a (u fa')) - ( first (iso-eq B (first is-rezk-B) fa fa' + ( fa) (fa') + ( all-left-adjoint-components-equal-is-rezk-is-segal) + ( ηa))) + ( ap (hom B fa fa') (hom A a (u fa')) + ( first + ( iso-eq B (first is-rezk-B) fa fa' ( all-left-adjoint-components-equal-is-rezk-is-segal))) - ( to-left-adjoint-components-is-rezk-is-segal) - ( ηa-transposition fa') - ( iso-eq-iso-to-left-adjoint-components-is-rezk)) - ( compute-covariant-transport-of-hom-family-is-segal A is-segal-A - ( a) (u fa) (u fa') ( ηa) - ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) - ( compute-covariant-transport-of-substitution A B (hom A a) - ( is-covariant-representable-is-segal A is-segal-A a) u - ( fa) ( fa') - ( to-left-adjoint-components-is-rezk-is-segal) - ( ηa)) - ( triangle-to-left-adjoint-components-is-rezk-is-segal) + ( to-left-adjoint-components-is-rezk-is-segal) + ( ηa-transposition fa') + ( iso-eq-iso-to-left-adjoint-components-is-rezk)) + ( compute-covariant-transport-of-hom-family-is-segal A is-segal-A + ( a) (u fa) (u fa') ( ηa) + ( ap-hom B A u fa fa' to-left-adjoint-components-is-rezk-is-segal)) + ( compute-covariant-transport-of-substitution A B (hom A a) + ( is-covariant-representable-is-segal A is-segal-A a) u (fa) (fa') + ( to-left-adjoint-components-is-rezk-is-segal) + ( ηa)) + ( triangle-to-left-adjoint-components-is-rezk-is-segal) #def all-unit-components-equal-is-rezk-is-segal uses (extext A is-segal-A u a ω ω') : (fa, ηa) =_{Σ (b : B), hom A a (u b)} (fa', ηa') := - path-of-pairs-pair-of-paths B (\ b → hom A a (u b)) ( fa) ( fa') - ( all-left-adjoint-components-equal-is-rezk-is-segal) - ( ηa) ( ηa') - compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal + path-of-pairs-pair-of-paths B (\ b → hom A a (u b)) (fa) (fa') + ( all-left-adjoint-components-equal-is-rezk-is-segal) + ( ηa) ( ηa') + ( compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal) #end all-unit-arrows-equal-is-rezk-is-segal ``` From 1d0ef54e321855d69733f67f69d86fd549c79a57 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sun, 22 Oct 2023 17:19:04 -0400 Subject: [PATCH 7/7] the equivalence between the type we want to prove is a proposition and the type in which all elements are equal --- src/hott/05-sigma.rzk.md | 17 ++- src/simplicial-hott/11-adjunctions.rzk.md | 166 +++++++++++++++++++++- 2 files changed, 179 insertions(+), 4 deletions(-) diff --git a/src/hott/05-sigma.rzk.md b/src/hott/05-sigma.rzk.md index 6ae35852..ae4e4095 100644 --- a/src/hott/05-sigma.rzk.md +++ b/src/hott/05-sigma.rzk.md @@ -536,7 +536,20 @@ This is the dependent version of the currying equivalence. ( B : A → U) ( C : (x : A) → B x → U) : Equiv - ( (x : A) → Σ (y : B x) , C x y) - ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x)) + ( (x : A) → Σ (y : B x) , C x y) + ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x)) := (choice A B C , is-equiv-choice A B C) + +#def inv-equiv-choice + ( A : U) + ( B : A → U) + ( C : (x : A) → B x → U) + : Equiv + ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x)) + ( (x : A) → Σ (y : B x) , C x y) + := + inv-equiv + ( (x : A) → Σ (y : B x) , C x y) + ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x)) + ( equiv-choice A B C) ``` diff --git a/src/simplicial-hott/11-adjunctions.rzk.md b/src/simplicial-hott/11-adjunctions.rzk.md index 49079766..cc839c3e 100644 --- a/src/simplicial-hott/11-adjunctions.rzk.md +++ b/src/simplicial-hott/11-adjunctions.rzk.md @@ -1088,9 +1088,9 @@ of `#!rzk is-transposing-right-adj A B u` ```rzk #section all-unit-arrows-equal-is-rezk-is-segal -#variables A B : U -#variable is-segal-A : is-segal A +#variables B A : U #variable is-rezk-B : is-rezk B +#variable is-segal-A : is-segal A #variable u : B → A #variable a : A #variables fa fa' : B @@ -1440,4 +1440,166 @@ of `#!rzk is-transposing-right-adj A B u` ( compute-transport-all-left-adjoint-components-equal-is-rezk-is-segal) #end all-unit-arrows-equal-is-rezk-is-segal + +#def is-transposing-unit + ( B A : U) + ( is-segal-A : is-segal A) + ( u : B → A) + ( f : A → B) + ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + : U + := + ( a : A) → (b : B) + → is-equiv (hom B (f a) b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( \ t → η t a) + ( ap-hom B A u (f a) b k)) + +#def is-transposing-unit-components + ( B A : U) + ( is-segal-A : is-segal A) + ( u : B → A) + ( f : A → B) + ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + : U + := + ( a : A) → (b : B) + → is-equiv (hom B (f a) b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( η a) + ( ap-hom B A u (f a) b k)) + +#def equiv-transposing-unit-transposing-unit-components + ( B A : U) + ( is-segal-A : is-segal A) + ( u : B → A) + : Equiv + ( Σ (f : A → B) + , Σ ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit B A is-segal-A u f η) + ( Σ (f : A → B) + , Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + := + total-equiv-family-of-equiv + ( A → B) + ( \ f → + Σ ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit B A is-segal-A u f η) + ( \ f → + Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + ( \ f → + equiv-total-pullback-is-equiv + ( nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + ( ev-components-nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + ( is-equiv-ev-components-nat-trans A (\ _ → A) + ( identity A) (comp A B A u f)) + ( \ η → is-transposing-unit-components B A is-segal-A u f η)) + +#def equiv-choice-transposing-unit-components + ( B A : U) + ( is-segal-A : is-segal A) + ( u : B → A) + : Equiv + ( Σ (f : A → B) + , Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + ( (a : A) + → Σ (fa : B) + , Σ ( ηa : hom A a (u fa)) + , ( b : B) + → is-equiv (hom B fa b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u fa) (u b) + ( ηa) (ap-hom B A u fa b k))) + := + equiv-comp + ( Σ (f : A → B) + , Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + ( Σ (f : A → B) + , (a : A) → + Σ ( ηa : hom A a (u (f a))) + , ( b : B) + → is-equiv (hom B (f a) b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( ηa) (ap-hom B A u (f a) b k))) + ( ( a : A) + → Σ (fa : B) + , Σ ( ηa : hom A a (u fa)) + , ( b : B) + → is-equiv (hom B fa b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u fa) (u b) + ( ηa) (ap-hom B A u fa b k))) + ( total-equiv-family-of-equiv + ( A → B) + ( \ f → + Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + ( \ f → + (a : A) + → Σ ( ηa : hom A a (u (f a))) + , ( b : B) + → is-equiv (hom B (f a) b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( ηa) + ( ap-hom B A u (f a) b k))) + ( \ f → + inv-equiv-choice A ( \ a → hom A a (u (f a))) + ( \ a ηa → + ( b : B) + → is-equiv (hom B (f a) b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u (f a)) (u b) + ( ηa) (ap-hom B A u (f a) b k))))) + ( inv-equiv-choice A ( \ _ → B) + ( \ a fa → + Σ ( ηa : hom A a (u fa)) + , ( b : B) + → is-equiv (hom B fa b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u fa) (u b) + ( ηa) (ap-hom B A u fa b k)))) + +#def equiv-choice-transposing-unit + ( B A : U) + ( is-segal-A : is-segal A) + ( u : B → A) + : Equiv + ( Σ (f : A → B) + , Σ ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit B A is-segal-A u f η) + ( (a : A) + → Σ (fa : B) + , Σ ( ηa : hom A a (u fa)) + , ( b : B) + → is-equiv (hom B fa b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u fa) (u b) + ( ηa) (ap-hom B A u fa b k))) + := + equiv-comp + ( Σ (f : A → B) + , Σ ( η : nat-trans A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit B A is-segal-A u f η) + ( Σ (f : A → B) + , Σ ( η : nat-trans-components A (\ _ → A) (identity A) (comp A B A u f)) + , is-transposing-unit-components B A is-segal-A u f η) + ( (a : A) + → Σ (fa : B) + , Σ ( ηa : hom A a (u fa)) + , ( b : B) + → is-equiv (hom B fa b) (hom A a (u b)) + ( \ k → + comp-is-segal A is-segal-A a (u fa) (u b) + ( ηa) (ap-hom B A u fa b k))) + ( equiv-transposing-unit-transposing-unit-components B A is-segal-A u) + ( equiv-choice-transposing-unit-components B A is-segal-A u) ```