From c56d02aebc4d538a24162298266f896825dc69a1 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 22:23:30 +0200 Subject: [PATCH 1/4] equivalences are right orthogonal --- .../04-right-orthogonal.rzk.md | 49 ++++++++++++++++++- 1 file changed, 48 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 7a7d53b2..1bb038cf 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -8,11 +8,13 @@ This is a literate `rzk` file: ## Prerequisites -Some of the definitions in this file rely on extension extensionality: +Some of the definitions in this file rely on extension extensionality +or function extensionality: ```rzk #assume naiveextext : NaiveExtExt #assume extext : ExtExt +#assume funext : FunExt ``` ## Right orthogonal maps with respect to shapes @@ -380,6 +382,51 @@ stability properties of maps right orthogonal to it. #variable ϕ : ψ → TOPE ``` +### Equivalences are right orthogonal + +Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. + +```rzk +#def is-right-orthogonal-to-shape-is-equiv uses (extext) + ( A' A : U) + ( α : A' → A) + ( is-equiv-α : is-equiv A' A α) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-homotopy-cartesian-is-horizontal-equiv + ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( second + ( equiv-extension-equiv-family extext I ( \ t → ϕ t) + ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α)))) + ( is-equiv-Equiv-is-equiv' + ( ψ → A') ( ψ → A) ( \ τ' t → α (τ' t)) + ( Σ (σ' : ϕ → A') , (t : ψ) → A' [ϕ t ↦ σ' t]) + ( Σ (σ : ϕ → A) , (t : ψ) → A [ϕ t ↦ σ t]) + ( \ (σ' , τ') → ( \ t → α (σ' t) , \ t → α (τ' t))) + ( cofibration-composition-functorial I ψ ϕ ( \ _ → BOT) + ( \ _ → A') ( \ _ → A) ( \ _ → α) ( \ _ → recBOT)) + ( second + ( equiv-extension-equiv-family extext I ( \ t → ψ t) + ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α))))) +``` + +Right orthogonality is closed under homotopy. + +```rzk +#def is-right-orthogonal-homotopy-to-shape uses (funext) + ( A' A : U) + ( α β : A' → A) + ( h : homotopy A' A α β) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + → is-right-orthogonal-to-shape I ψ ϕ A' A β + := + transport (A' → A) ( is-right-orthogonal-to-shape I ψ ϕ A' A) α β + ( first (first (funext A' (\ _ → A) α β)) h) +``` + ### Stability under composition ```rzk From a875410e7c68daeaad7db10067fc3e00924a8024 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 23:53:41 +0200 Subject: [PATCH 2/4] weak left cancellation with section, closed under equiv of maps --- src/hott/11-homotopy-pullbacks.rzk.md | 23 +++++ src/simplicial-hott/03-extension-types.rzk.md | 21 +++++ .../04-right-orthogonal.rzk.md | 88 +++++++++++++++++-- 3 files changed, 124 insertions(+), 8 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 6fdbd16c..bf258092 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -409,6 +409,29 @@ from composition and cancelling laws for equivalences. ( ihc (f' a'')) ( ihc'' a'') +``` + +We can cancel the left homotopy cartesian square if its lower map +`f' : A'' → A'` has a section. + +```rzk +#def is-homotopy-cartesian-left-cancel-with-lower-section + ( has-section-f' : has-section A'' A' f') + ( ihc' : is-homotopy-cartesian A'' C'' A' C' f' F') + ( ihc'' : is-homotopy-cartesian A'' C'' A C + ( comp A'' A' A f f') + ( \ a'' → + comp (C'' a'') (C' (f' a'')) (C (f (f' a''))) + (F (f' a'')) (F' a''))) + : is-homotopy-cartesian A' C' A C f F + := + ind-has-section A'' A' f' has-section-f' + ( \ a' → is-equiv (C' a') (C (f a')) (F a')) + ( \ a'' → + is-equiv-left-factor (C'' a'') (C' (f' a'')) (C (f (f' a''))) + ( F' a'') (ihc' a'') + ( F (f' a'')) ( ihc'' a'')) + #end homotopy-cartesian-horizontal-calculus ``` diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index c9abd137..0ecd2cff 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -706,6 +706,7 @@ We now assume extension extensionality and derive a few consequences. ```rzk #assume extext : ExtExt +#assume naiveextext : NaiveExtExt ``` In particular, extension extensionality implies that homotopies give rise to @@ -762,6 +763,26 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`. ( \ t → second (second (second (famequiv t))) (b t)))))) ``` +Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a +section on extension types + +```rzk +#def has-section-extension-has-section-family uses (naiveextext) + ( I : CUBE) + ( ψ : I → TOPE) + ( A B : ψ → U) + ( f : ( t : ψ) → A t → B t) + ( has-fiberwise-section-f : (t : ψ) → has-section (A t ) (B t) (f t)) + : has-section ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t)) + := + ( ( \ b t → first (has-fiberwise-section-f t) (b t)) + , \ b → + ( naiveextext I ψ (\ _ → BOT) B (\ _ → recBOT) + ( \ t → f t (first (has-fiberwise-section-f t) (b t))) + ( \ t → b t) + ( \ t → second (has-fiberwise-section-f t) (b t)))) +``` + We have a homotopy extension property. The following code is another instantiation of casting, necessary for some diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 1bb038cf..8bc650ec 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -387,7 +387,7 @@ stability properties of maps right orthogonal to it. Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. ```rzk -#def is-right-orthogonal-to-shape-is-equiv uses (extext) +#def is-right-orthogonal-is-equiv-to-shape uses (extext) ( A' A : U) ( α : A' → A) ( is-equiv-α : is-equiv A' A α) @@ -463,13 +463,36 @@ Right orthogonality is closed under homotopy. := \ σ'' → is-equiv-right-factor - ( extension-type I ψ ϕ (\ _ → A'') σ'') - ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t))) - ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t)))) - ( \ τ'' t → α' (τ'' t)) - ( \ τ' t → α (τ' t)) - ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) - ( is-orth-ψ-ϕ-αα' σ'') + ( extension-type I ψ ϕ (\ _ → A'') σ'') + ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t))) + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t)))) + ( \ τ'' t → α' (τ'' t)) + ( \ τ' t → α (τ' t)) + ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) + ( is-orth-ψ-ϕ-αα' σ'') +``` + +### Left cancellation with section (weak version) + +This should hold even without assuming `is-orth-ψ-ϕ-α'`. + +```rzk +#def is-right-orthogonal-weak-left-cancel-with-section-to-shape + uses (naiveextext is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-αα') + ( has-section-α' : has-section A'' A' α') + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-homotopy-cartesian-left-cancel-with-lower-section + ( ϕ → A'' ) ( \ σ'' → (t : ψ) → A'' [ϕ t ↦ σ'' t]) + ( ϕ → A' ) ( \ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A ) ( \ σ → (t : ψ) → A [ϕ t ↦ σ t]) + ( \ σ'' t → α' (σ'' t)) ( \ _ τ'' x → α' (τ'' x) ) + ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) ) + ( has-section-extension-has-section-family naiveextext I (\ t → ϕ t) + ( \ _ → A'') (\ _ → A') (\ _ → α') + ( \ _ → has-section-α')) + ( is-orth-ψ-ϕ-α') + ( is-orth-ψ-ϕ-αα') ``` ### Stability under pullback @@ -627,6 +650,55 @@ Then we can deduce that right orthogonal maps are preserved under pullback: #end right-orthogonal-calculus ``` +### Right orthogonal maps are closed under equivalence + +If two maps `α : A' → A` and `β : B' → B` are equivalent, +then if one is right orthogonal to `ϕ ⊂ ψ`, then so is the other. + +```rzk +#section is-right-orthogonal-equiv-to-shape + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : U +#variable α : A' → A +#variables B' B : U +#variable β : B' → B + +#def is-right-orthogonal-equiv-to-shape uses (funext extext) + ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β) + ( is-orth-ψ-ϕ-β : is-right-orthogonal-to-shape I ψ ϕ B' B β) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-right-orthogonal-right-cancel-to-shape I ψ ϕ A' A B α s + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s) + ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B + ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η) + ( is-right-orthogonal-comp-to-shape I ψ ϕ A' B' B s' β + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s') + ( is-orth-ψ-ϕ-β))) + +#def is-right-orthogonal-equiv-to-shape' + uses (funext extext naiveextext) + ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β) + ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : is-right-orthogonal-to-shape I ψ ϕ B' B β + := + is-right-orthogonal-weak-left-cancel-with-section-to-shape + I ψ ϕ A' B' B s' β + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s') + ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B + ( \ a' → s (α a')) ( \ a' → β (s' a')) + ( rev-homotopy A' B ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η)) + ( is-right-orthogonal-comp-to-shape I ψ ϕ A' A B α s + ( is-orth-ψ-ϕ-α) + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s))) + ( second is-equiv-s') + +#end is-right-orthogonal-equiv-to-shape +``` + ## Types with unique extension We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, if From 32c9f9cc0c2e4b956523c5a15f43e431a49ee253 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 23:58:48 +0200 Subject: [PATCH 3/4] autoformat --- src/simplicial-hott/03-extension-types.rzk.md | 4 ++-- src/simplicial-hott/04-right-orthogonal.rzk.md | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 0ecd2cff..33593678 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -763,8 +763,8 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`. ( \ t → second (second (second (famequiv t))) (b t)))))) ``` -Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a -section on extension types +Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a section +on extension types ```rzk #def has-section-extension-has-section-family uses (naiveextext) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 8bc650ec..5f0ab1f3 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -8,8 +8,8 @@ This is a literate `rzk` file: ## Prerequisites -Some of the definitions in this file rely on extension extensionality -or function extensionality: +Some of the definitions in this file rely on extension extensionality or +function extensionality: ```rzk #assume naiveextext : NaiveExtExt @@ -652,8 +652,8 @@ Then we can deduce that right orthogonal maps are preserved under pullback: ### Right orthogonal maps are closed under equivalence -If two maps `α : A' → A` and `β : B' → B` are equivalent, -then if one is right orthogonal to `ϕ ⊂ ψ`, then so is the other. +If two maps `α : A' → A` and `β : B' → B` are equivalent, then if one is right +orthogonal to `ϕ ⊂ ψ`, then so is the other. ```rzk #section is-right-orthogonal-equiv-to-shape From 65cfff1a6563d49b4610888ae5a24bc98b556e88 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 10:29:35 +0200 Subject: [PATCH 4/4] add actual left-cancel-with-section to homotopy-cartesian --- src/hott/11-homotopy-pullbacks.rzk.md | 21 +++++++++++++++++++ src/simplicial-hott/03-extension-types.rzk.md | 4 ++++ 2 files changed, 25 insertions(+) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index bf258092..5783d68f 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -431,6 +431,27 @@ We can cancel the left homotopy cartesian square if its lower map is-equiv-left-factor (C'' a'') (C' (f' a'')) (C (f (f' a''))) ( F' a'') (ihc' a'') ( F (f' a'')) ( ihc'' a'')) +``` + +In fact, it suffices to assume that the left square has horizontal sections. + +```rzk +#def is-homotopy-cartesian-left-cancel-with-section + ( has-section-f' : has-section A'' A' f') + ( has-sections-F' : (a'' : A'') → has-section (C'' a'') (C' (f' a'')) (F' a'')) + ( ihc'' : is-homotopy-cartesian A'' C'' A C + ( comp A'' A' A f f') + ( \ a'' → + comp (C'' a'') (C' (f' a'')) (C (f (f' a''))) + (F (f' a'')) (F' a''))) + : is-homotopy-cartesian A' C' A C f F + := + ind-has-section A'' A' f' has-section-f' + ( \ a' → is-equiv (C' a') (C (f a')) (F a')) + ( \ a'' → + is-equiv-left-cancel (C'' a'') (C' (f' a'')) (C (f (f' a''))) + ( F' a'') ( has-sections-F' a'') + ( F (f' a'')) ( ihc'' a'')) #end homotopy-cartesian-horizontal-calculus ``` diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 33593678..1af91e74 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -725,6 +725,8 @@ retraction to `#!rzk ext-htpy-eq`. := first (first (extext I ψ ϕ A a f g)) ``` +### Functoriality properties of extension types + By extension extensionality, fiberwise equivalences of extension types define equivalences of extension types. For simplicity, we extend from `#!rzk BOT`. @@ -783,6 +785,8 @@ on extension types ( \ t → second (has-fiberwise-section-f t) (b t)))) ``` +### Homotopy extension property + We have a homotopy extension property. The following code is another instantiation of casting, necessary for some