From 59f7a49481f1e76215c11b60bd44e611dd313b12 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 15:21:44 +0200 Subject: [PATCH 01/14] composition and right cancel of right orthogonal maps --- .../04-right-orthogonal.rzk.md | 58 +++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 802fb1a4..65678a23 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -303,6 +303,64 @@ then so is `ψ ⊂ ϕ ∪ ψ`. ( is-orth-ϕ-ψ∧ϕ ( \ t → τ' t)) ``` +## Stability properties of right orthogonal maps + +Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate +stability properties of maps right orthogonal to it. + +```rzk +#section right-orthogonal-calculus +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +``` + +### Stability under composition + +```rzk +#variables A'' A' A : U +#variable α' : A'' → A' +#variable α : A' → A + +#def is-right-orthogonal-comp-to-shape + ( is-orth-ψ-ϕ-α' : is-right-orthogonal-to-shape I ψ ϕ A'' A' α') + ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : is-right-orthogonal-to-shape I ψ ϕ A'' A (comp A'' A' A α α') + := + \ σ'' → + is-equiv-comp + ( extension-type I ψ ϕ (\ _ → A'') σ'') + ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t))) + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t)))) + ( \ τ'' t → α' (τ'' t)) + ( is-orth-ψ-ϕ-α' σ'') + ( \ τ' t → α (τ' t)) + ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) + +``` + +### Right cancellation + +```rzk +#def is-right-orthogonal-right-cancel-to-shape + ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + ( is-orth-ψ-ϕ-αα' : is-right-orthogonal-to-shape I ψ ϕ A'' A + ( comp A'' A' A α α')) + : is-right-orthogonal-to-shape I ψ ϕ A'' A' α' + := + \ σ'' → + 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-ψ-ϕ-αα' σ'') + +#end right-orthogonal-calculus +``` + ## Types with unique extension We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, From 129303c14f51204e81908ac91c459c1505df9ea4 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 17:28:44 +0200 Subject: [PATCH 02/14] better formatting --- .../04-right-orthogonal.rzk.md | 57 ++++++++----------- 1 file changed, 24 insertions(+), 33 deletions(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 965593fd..2ac2483d 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -106,10 +106,10 @@ occasionally go back or forth along the functorial equivalence ( ( t : ψ) → A' [ϕ t ↦ σ' t]) ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) ( \ υ' t → α ( υ' t)) - ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]), - ( ( t : ψ) → A' [χ t ↦ τ' t])) - ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]), - ( ( t : ψ) → A [χ t ↦ τ t])) + ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]) + , ( ( t : ψ) → A' [χ t ↦ τ' t])) + ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]) + , ( ( t : ψ) → A [χ t ↦ τ t])) ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t))) ( cofibration-composition-functorial I ψ χ ϕ ( \ _ → A') ( \ _ → A) ( \ _ → α) σ') @@ -130,10 +130,10 @@ Left orthogonal shape inclusions are preserved under composition. ( ( t : ψ) → A' [ϕ t ↦ σ' t]) ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) ( \ υ' t → α ( υ' t)) - ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]), - ( ( t : ψ) → A' [χ t ↦ τ' t])) - ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]), - ( ( t : ψ) → A [χ t ↦ τ t])) + ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]) + , ( ( t : ψ) → A' [χ t ↦ τ' t])) + ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]) + , ( ( t : ψ) → A [χ t ↦ τ t])) ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t))) ( cofibration-composition-functorial I ψ χ ϕ ( \ _ → A') ( \ _ → A) ( \ _ → α) σ') @@ -174,7 +174,7 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i ( is-orth-χ-ϕ ) (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) ( \ ( t : ϕ) → τ' t) - τ' + ( τ') ``` If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` and `χ ⊂ ψ` is a (functorial) @@ -196,7 +196,7 @@ shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`. ( \ _ τ' x → α (τ' x) ) ( \ _ _ υ' x → α (υ' x) ) ( relativize-is-functorial-shape-retract I ψ χ is-fretract-ψ-χ ϕ A' A α) - (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) + ( is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) #end left-orthogonal-calculus-1 ``` @@ -224,12 +224,10 @@ naive form of) extension extensionality. ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α := \ ( σ' : ( (t,s) : J × I | χ t ∧ ϕ s) → A') → - ( - ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))]) + ( ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))]) ( t, s) → ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s - , - \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) → + , \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) → naiveextext ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) ( \ _ → A') @@ -245,15 +243,11 @@ naive form of) extension extensionality. ( \ s' → τ' (t, s') ) ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ' (t, s'))) - ( s) - ) - ) - , - ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) + ( s))) + , ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) ( t, s) → ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s - , - \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) → + , \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) → naiveextext ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) ( \ _ → A) @@ -267,14 +261,11 @@ naive form of) extension extensionality. ( \ s'' → α ( ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) - (s''))) + ( s''))) ( \ s' → τ (t, s') ) ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s'))) - ( s) - ) - ) - ) + ( s)))) ``` ### Stability under exact pushouts @@ -372,8 +363,7 @@ for each `σ : ϕ → A` the type of `ψ`-extensions is contractible. ( ϕ : ψ → TOPE) ( A : U) : U - := - ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t]) + := ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t]) ``` The property of having unique extension can be pulled back along any right @@ -424,11 +414,11 @@ fiber of the restriction map `(ψ → A) → (ϕ → A)`. := is-equiv-is-contr-map (ψ → A) (ϕ → A) ( \ τ t → τ t) ( \ ( σ : ϕ → A) → - is-contr-equiv-is-contr - ( extension-type I ψ ϕ ( \ t → A) σ) - ( homotopy-extension-type I ψ ϕ ( \ t → A) σ) - ( extension-type-weakening I ψ ϕ ( \ t → A) σ) - ( has-ue-ψ-ϕ-A σ)) + is-contr-equiv-is-contr + ( extension-type I ψ ϕ ( \ t → A) σ) + ( homotopy-extension-type I ψ ϕ ( \ t → A) σ) + ( extension-type-weakening I ψ ϕ ( \ t → A) σ) + ( has-ue-ψ-ϕ-A σ)) #def has-unique-extensions-is-local-type ( is-lt-ψ-ϕ-A : is-local-type) @@ -443,6 +433,7 @@ fiber of the restriction map `(ψ → A) → (ϕ → A)`. ( ψ → A) (ϕ → A) ( \ τ t → τ t) ( is-lt-ψ-ϕ-A) ( σ)) + #end is-local-type ``` From 0dbbcb9d940a2f5b9b69a58d75ed39567246677e Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 17:54:45 +0200 Subject: [PATCH 03/14] write statement (no proof yet) --- .../04-right-orthogonal.rzk.md | 29 +++++++++++++++---- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 2ac2483d..a5d3d88a 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -312,9 +312,13 @@ stability properties of maps right orthogonal to it. #variable α' : A'' → A' #variable α : A' → A +#variable is-orth-ψ-ϕ-α' : is-right-orthogonal-to-shape I ψ ϕ A'' A' α' +#variable is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α +#variable is-orth-ψ-ϕ-αα' : is-right-orthogonal-to-shape I ψ ϕ A'' A + ( comp A'' A' A α α') + #def is-right-orthogonal-comp-to-shape - ( is-orth-ψ-ϕ-α' : is-right-orthogonal-to-shape I ψ ϕ A'' A' α') - ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + uses (is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-α) : is-right-orthogonal-to-shape I ψ ϕ A'' A (comp A'' A' A α α') := \ σ'' → @@ -326,16 +330,13 @@ stability properties of maps right orthogonal to it. ( is-orth-ψ-ϕ-α' σ'') ( \ τ' t → α (τ' t)) ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) - ``` ### Right cancellation ```rzk #def is-right-orthogonal-right-cancel-to-shape - ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) - ( is-orth-ψ-ϕ-αα' : is-right-orthogonal-to-shape I ψ ϕ A'' A - ( comp A'' A' A α α')) + uses (is-orth-ψ-ϕ-α is-orth-ψ-ϕ-αα') : is-right-orthogonal-to-shape I ψ ϕ A'' A' α' := \ σ'' → @@ -347,6 +348,22 @@ stability properties of maps right orthogonal to it. ( \ τ' t → α (τ' t)) ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) ( is-orth-ψ-ϕ-αα' σ'') +``` + +### Stability under pullback + +Right orthogonal maps are stable under pullback. + +```rzk +#variable B : U +#variable f : B → A + +#def is-right-orthogonal-pullback-to-shape + uses (is-orth-ψ-ϕ-α) + : is-right-orthogonal-to-shape I ψ ϕ + ( fiber-product A B f A' α) + ( B) ( first-fiber-product A B f A' α) + := undefined #end right-orthogonal-calculus ``` From 63668150627fcf21e4070faa5b8a4b0f8770bb28 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 23:01:11 +0200 Subject: [PATCH 04/14] set up helper theory of generalized relative extension types --- src/hott/03-equivalences.rzk.md | 60 +++-- src/simplicial-hott/03-extension-types.rzk.md | 68 +++++- .../04-right-orthogonal.rzk.md | 218 +++++++++++++++++- 3 files changed, 319 insertions(+), 27 deletions(-) diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index a1f238ef..36b391cd 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -24,18 +24,6 @@ This is a literate `rzk` file: := Σ (r : B → A) , (homotopy A A (comp A B A r f) (identity A)) ``` -```rzk -#def ind-has-section - ( f : A → B) - ( ( sec-f , ε-f) : has-section f) - ( C : B → U) - ( s : ( a : A) → C ( f a)) - ( b : B) - : C b - := - transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b)) -``` - We define equivalences to be bi-invertible maps. ```rzk @@ -70,9 +58,17 @@ We define equivalences to be bi-invertible maps. : B → A := first (second is-equiv-f) +#def has-section-is-equiv + : has-section A B f + := second is-equiv-f + #def retraction-is-equiv uses (f) : B → A := first (first is-equiv-f) + +#def has-retraction-is-equiv + : has-retraction A B f + := first is-equiv-f ``` ```rzk title="The homotopy between the section and retraction of an equivalence" @@ -214,7 +210,7 @@ The inverse of an invertible map has an inverse. first ( second has-inverse-f))) ``` -## Composing equivalences +## The type of equivalences The type of equivalences between types uses `#!rzk is-equiv` rather than `#!rzk has-inverse`. @@ -226,6 +222,34 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than := Σ (f : A → B) , (is-equiv A B f) ``` +## Induction with section + +```rzk +#def ind-has-section + ( A B : U) + ( f : A → B) + ( ( sec-f , ε-f) : has-section A B f) + ( C : B → U) + ( s : ( a : A) → C ( f a)) + ( b : B) + : C b + := + transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b)) +``` + +It is convenient to have available the special case where `f` is an equivalence. + +```rzk +#def ind-has-section-equiv + ( A B : U) + ( (f, is-equiv-f) : Equiv A B) + : ( C : B → U) → (( a : A) → C ( f a)) → ( b : B) → C b + := + ind-has-section A B f (second is-equiv-f) +``` + +## Composing equivalences + The data of an equivalence is not symmetric so we promote an equivalence to an invertible map to prove symmetry: @@ -688,6 +712,16 @@ dependent function types. := (rev A x y , ((rev A y x , rev-rev A x y) , (rev A y x , rev-rev A y x))) ``` +```rzk +#def ind-rev + ( A : U) + ( x y : A) + ( B : (x = y) → U) + : ((p : y = x) → B (rev A y x p)) → ( q : x = y) → B q + := + ind-has-section-equiv (y = x) (x = y) (equiv-rev A y x) ( B) +``` + ## Concatenation with a fixed path is an equivalence ```rzk diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index f16ca147..51b3ddeb 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -48,7 +48,7 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of := \ τ → ( τ, refl) -#def extension-type-weakening-section +#def section-extension-type-weakening' : ( σ : (t : ϕ) → A t) → ( th : homotopy-extension-type σ) → Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th) @@ -63,17 +63,24 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of ( σ : (t : ϕ) → A t) : (homotopy-extension-type σ) → (extension-type σ) := - \ th → first (extension-type-weakening-section σ th) + \ th → first (section-extension-type-weakening' σ th) + +#def has-section-extension-type-weakening + ( σ : (t : ϕ) → A t) + : has-section (extension-type σ) (homotopy-extension-type σ) + (extension-type-weakening-map σ) + := + ( extension-strictification σ, + \ th → ( second (section-extension-type-weakening' σ th))) + #def is-equiv-extension-type-weakening ( σ : (t : ϕ) → A t) : is-equiv (extension-type σ) (homotopy-extension-type σ) (extension-type-weakening-map σ) := - ( ( extension-strictification σ , - \ _ → refl), - ( extension-strictification σ, - \ th → ( second (extension-type-weakening-section σ th)))) + ( ( extension-strictification σ, \ _ → refl) + , has-section-extension-type-weakening σ) #def extension-type-weakening ( σ : (t : ϕ) → A t) @@ -116,7 +123,6 @@ This equivalence is functorial in the following sense: , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t)) ) ) - ``` ## Commutation of arguments and currying @@ -1057,3 +1063,51 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r ( a) ( f)))) ``` + +### Pointwise homotopy extension types + +Using `ExtExt` we can write the homotopy in the homotopy extension type pointwise. + +```rzk +#section pointwise-homotopy-extension-type + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variable A : ψ → U + +#def pointwise-homotopy-extension-type + ( σ : (t : ϕ) → A t) + : U + := + Σ ( τ : (t : ψ) → A t) , ( (t : ϕ) → (τ t =_{ A t} σ t)) + +#def equiv-pointwise-homotopy-extension-type uses (extext) + ( σ : (t : ϕ) → A t) + : Equiv + ( homotopy-extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + := + total-equiv-family-equiv + ( (t : ψ) → A t) + ( \ τ → (\ t → τ t) =_{ (t : ϕ) → A t} σ) + ( \ τ → (t : ϕ) → (τ t = σ t)) + ( \ τ → + equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t) + ( \ _ → recBOT) ( \ t → τ t) ( σ)) + +#def extension-type-pointwise-weakening uses (extext) + ( σ : (t : ϕ) → A t) + : Equiv + ( extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + := equiv-comp + ( extension-type I ψ ϕ A σ) + ( homotopy-extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + ( extension-type-weakening I ψ ϕ A σ) + ( equiv-pointwise-homotopy-extension-type σ) + + +#end pointwise-homotopy-extension-type +``` diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index a5d3d88a..3cd83dcd 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -8,10 +8,11 @@ This is a literate `rzk` file: ## Prerequisites -Some of the definitions in this file rely on naive extension extensionality: +Some of the definitions in this file rely on extension extensionality: ```rzk #assume naiveextext : NaiveExtExt +#assume extext : ExtExt ``` ## Right orthogonal maps with respect to shapes @@ -52,6 +53,161 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) ) ``` +## Relative extension types + +Using `ExtExt`, we can characterize right orthogonal maps +in terms of the contractibility of _relative extension types_. + +```rzk +#section relative-extension-types + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : U +#variable α : A' → A + +#def relative-extension-type + ( σ' : ϕ → A') + ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + : U + := + Σ ( τ' : (t : ψ) → A' [ϕ t ↦ σ' t]) + , ( t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ refl] + +#def equiv-relative-extension-type-fib uses (extext) + ( σ' : ϕ → A') + ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + : Equiv + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type σ' τ) + := + total-equiv-family-equiv + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( \ τ' → (\ t → α (τ' t)) =_{ (t : ψ) → A [ϕ t ↦ α (σ' t)]} τ) + ( \ τ' → (t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ refl]) + ( \ τ' → + equiv-ExtExt extext I ψ ϕ (\ _ → A) (\ t → α (σ' t)) + ( \ t → α (τ' t)) ( τ)) + +#def has-contr-relative-extension-types + : U + := + ( σ' : ϕ → A') + → ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + → ( is-contr (relative-extension-type σ' τ)) + +#def has-contr-relative-extension-types-is-right-orthogonal uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-contr-relative-extension-types + := + \ σ' τ → + is-contr-equiv-is-contr + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type σ' τ) + ( equiv-relative-extension-type-fib σ' τ) + ( is-contr-map-is-equiv + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( is-orth-α σ') + ( τ)) + +#def is-right-orthogonal-has-contr-relative-extension-types uses (extext) + ( are-contr-relext-α : has-contr-relative-extension-types) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + \ σ' → + is-equiv-is-contr-map + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( \ τ → + is-contr-equiv-is-contr' + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type σ' τ) + ( equiv-relative-extension-type-fib σ' τ) + ( are-contr-relext-α σ' τ) + ) +``` + +### Generalized relative extension types + +We will also need to allow more general relative extension types, +where we start with a `τ : ψ → A` that does not strictly restrict to +`\ t → α (σ' t)`. + +```rzk +#def general-relative-extension-type + ( σ' : ϕ → A') + ( τ : ψ → A) + ( h : (t : ϕ) → α (σ' t) = τ t) + : U + := + Σ ( τ' : (t : ψ) → A' [ϕ t ↦ σ' t]) + , ( t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ h t] +``` + +If all ordinary relative extension types are contractible, +then also all generalized ones. + +```rzk +#def has-contr-relative-extension-types-generalize' uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + ( σ' : ϕ → A') + ( τ : ψ → A) + ( h : (t : ϕ) → α (σ' t) = τ t) + : is-contr + ( general-relative-extension-type σ' τ + ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t)))) + := + ind-has-section-equiv + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (σ' t))) + ( pointwise-homotopy-extension-type I ψ ϕ (\ _ → A) (\ t → α (σ' t))) + ( extension-type-pointwise-weakening extext I ψ ϕ + ( \ _ → A) (\ t → α (σ' t))) + ( \ (τ̂ , ĥ) → + is-contr + ( general-relative-extension-type σ' τ̂ + ( \ t → rev A (τ̂ t) (α (σ' t)) (ĥ t)))) + ( \ τ → has-contr-relext-α σ' τ) + ( τ , \ t → (rev A (α (σ' t)) (τ t) (h t))) + +#def has-contr-relative-extension-types-generalize uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + ( σ' : ϕ → A') + ( τ : ψ → A) + ( h : (t : ϕ) → α (σ' t) = τ t) + : is-contr ( general-relative-extension-type σ' τ h) + := + transport + ( (t : ϕ) → α (σ' t) = τ t) + ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ)) + ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t))) + ( h) + ( naiveextext-extext extext + ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α (σ' t ) = τ t) (\ _ → recBOT) + ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t))) + ( h) + ( \ t → rev-rev A (α (σ' t)) (τ t) (h t))) + ( has-contr-relative-extension-types-generalize' + has-contr-relext-α σ' τ h) + +#end relative-extension-types +``` + ## Stability properties of left orthogonal shape inclusions We fix a map `α : A' → A`. @@ -353,17 +509,65 @@ stability properties of maps right orthogonal to it. ### Stability under pullback Right orthogonal maps are stable under pullback. +More precisely: If `α : A' → A` is right orthogonal, +then so is the second projection +`relative-product A A' α B f → B` for every `f : B → A`. + +To prove this, we show that each relative extension type +of `relative-product A A' α B f → B`, +is equivalent to a generalized extension type for `A' → A`. ```rzk #variable B : U #variable f : B → A -#def is-right-orthogonal-pullback-to-shape - uses (is-orth-ψ-ϕ-α) - : is-right-orthogonal-to-shape I ψ ϕ - ( fiber-product A B f A' α) - ( B) ( first-fiber-product A B f A' α) - := undefined +#section relative-extension-type-pullback + +#variable σB' : ϕ → relative-product A A' α B f +#variable τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)] + +#def relative-extension-type-pullback-general-relative-extension-type + ( (τA', hA) + : general-relative-extension-type I ψ ϕ A' A α + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + : relative-extension-type I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + ( σB') ( τB) + := + ( \ t → ( (τA' t, τB t) , hA t) + , \ t → refl) + +#def general-relative-extension-type-relative-extension-type-pullback + ( (τB', hB) + : relative-extension-type I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + ( σB') ( τB)) + : general-relative-extension-type I ψ ϕ A' A α + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t)) + := + ( \ t → first-relative-product A A' α B f (τB' t) + , \ t → + concat A + ( α (first-relative-product A A' α B f (τB' t))) + ( f (second-relative-product A A' α B f (τB' t))) + ( f (τB t)) + ( homotopy-relative-product A A' α B f (τB' t)) + ( ap B A + ( second-relative-product A A' α B f (τB' t)) + ( τB t) + ( f) ( hB t))) + + +#end relative-extension-type-pullback + + + #end right-orthogonal-calculus ``` From 77ebd95c140f97a7beeb256f545189c5f79e3d84 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 23:22:41 +0200 Subject: [PATCH 05/14] make all relative types properly dependent --- .../04-right-orthogonal.rzk.md | 197 ++++++++++-------- 1 file changed, 108 insertions(+), 89 deletions(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 3cd83dcd..c6641092 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -64,83 +64,42 @@ in terms of the contractibility of _relative extension types_. #variable I : CUBE #variable ψ : I → TOPE #variable ϕ : ψ → TOPE -#variables A' A : U -#variable α : A' → A +#variables A' A : ψ → U +#variable α : (t : ψ) → A' t → A t #def relative-extension-type - ( σ' : ϕ → A') - ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) : U := - Σ ( τ' : (t : ψ) → A' [ϕ t ↦ σ' t]) - , ( t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ refl] + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl] #def equiv-relative-extension-type-fib uses (extext) - ( σ' : ϕ → A') - ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) : Equiv ( fib - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + ( \ τ' t → α t (τ' t)) ( τ)) ( relative-extension-type σ' τ) := total-equiv-family-equiv - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( \ τ' → (\ t → α (τ' t)) =_{ (t : ψ) → A [ϕ t ↦ α (σ' t)]} τ) - ( \ τ' → (t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ refl]) + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ) + ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) ( \ τ' → - equiv-ExtExt extext I ψ ϕ (\ _ → A) (\ t → α (σ' t)) - ( \ t → α (τ' t)) ( τ)) + equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t)) + ( \ t → α t (τ' t)) ( τ)) #def has-contr-relative-extension-types : U := - ( σ' : ϕ → A') - → ( τ : (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( σ' : (t : ϕ) → A' t) + → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) → ( is-contr (relative-extension-type σ' τ)) - -#def has-contr-relative-extension-types-is-right-orthogonal uses (extext) - ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) - : has-contr-relative-extension-types - := - \ σ' τ → - is-contr-equiv-is-contr - ( fib - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( τ)) - ( relative-extension-type σ' τ) - ( equiv-relative-extension-type-fib σ' τ) - ( is-contr-map-is-equiv - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( is-orth-α σ') - ( τ)) - -#def is-right-orthogonal-has-contr-relative-extension-types uses (extext) - ( are-contr-relext-α : has-contr-relative-extension-types) - : is-right-orthogonal-to-shape I ψ ϕ A' A α - := - \ σ' → - is-equiv-is-contr-map - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( \ τ → - is-contr-equiv-is-contr' - ( fib - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( τ)) - ( relative-extension-type σ' τ) - ( equiv-relative-extension-type-fib σ' τ) - ( are-contr-relext-α σ' τ) - ) ``` ### Generalized relative extension types @@ -151,13 +110,13 @@ where we start with a `τ : ψ → A` that does not strictly restrict to ```rzk #def general-relative-extension-type - ( σ' : ϕ → A') - ( τ : ψ → A) - ( h : (t : ϕ) → α (σ' t) = τ t) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) : U := - Σ ( τ' : (t : ψ) → A' [ϕ t ↦ σ' t]) - , ( t : ψ) → (α (τ' t) = τ t) [ϕ t ↦ h t] + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] ``` If all ordinary relative extension types are contractible, @@ -166,48 +125,109 @@ then also all generalized ones. ```rzk #def has-contr-relative-extension-types-generalize' uses (extext) ( has-contr-relext-α : has-contr-relative-extension-types) - ( σ' : ϕ → A') - ( τ : ψ → A) - ( h : (t : ϕ) → α (σ' t) = τ t) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) : is-contr ( general-relative-extension-type σ' τ - ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t)))) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))) := ind-has-section-equiv - ( extension-type I ψ ϕ (\ _ → A) (\ t → α (σ' t))) - ( pointwise-homotopy-extension-type I ψ ϕ (\ _ → A) (\ t → α (σ' t))) - ( extension-type-pointwise-weakening extext I ψ ϕ - ( \ _ → A) (\ t → α (σ' t))) + ( extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( extension-type-pointwise-weakening extext I ψ ϕ A (\ t → α t (σ' t))) ( \ (τ̂ , ĥ) → is-contr ( general-relative-extension-type σ' τ̂ - ( \ t → rev A (τ̂ t) (α (σ' t)) (ĥ t)))) + ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t)))) ( \ τ → has-contr-relext-α σ' τ) - ( τ , \ t → (rev A (α (σ' t)) (τ t) (h t))) + ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t))) #def has-contr-relative-extension-types-generalize uses (extext) ( has-contr-relext-α : has-contr-relative-extension-types) - ( σ' : ϕ → A') - ( τ : ψ → A) - ( h : (t : ϕ) → α (σ' t) = τ t) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) : is-contr ( general-relative-extension-type σ' τ h) := transport - ( (t : ϕ) → α (σ' t) = τ t) + ( (t : ϕ) → α t (σ' t) = τ t) ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ)) - ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t))) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) ( h) ( naiveextext-extext extext - ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α (σ' t ) = τ t) (\ _ → recBOT) - ( \ t → rev A (τ t) (α (σ' t)) (rev A (α (σ' t)) (τ t) (h t))) + ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) ( h) - ( \ t → rev-rev A (α (σ' t)) (τ t) (h t))) + ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t))) ( has-contr-relative-extension-types-generalize' has-contr-relext-α σ' τ h) #end relative-extension-types ``` +### Characterization of right orthogonality + +```rzk +#section has-contr-relative-extension-types-iff-is-right-orthogonal + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : U +#variable α : A' → A + + +#def has-contr-relative-extension-types-is-right-orthogonal uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-contr-relative-extension-types I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + := + \ σ' τ → + is-contr-equiv-is-contr + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( equiv-relative-extension-type-fib I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( is-contr-map-is-equiv + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( is-orth-α σ') + ( τ)) + +#def is-right-orthogonal-has-contr-relative-extension-types uses (extext) + ( are-contr-relext-α + : has-contr-relative-extension-types I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α)) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + \ σ' → + is-equiv-is-contr-map + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( \ τ → + is-contr-equiv-is-contr' + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( equiv-relative-extension-type-fib I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( are-contr-relext-α σ' τ) + ) + +#end has-contr-relative-extension-types-iff-is-right-orthogonal +``` + ## Stability properties of left orthogonal shape inclusions We fix a map `α : A' → A`. @@ -528,13 +548,13 @@ is equivalent to a generalized extension type for `A' → A`. #def relative-extension-type-pullback-general-relative-extension-type ( (τA', hA) - : general-relative-extension-type I ψ ϕ A' A α + : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) ( \ t → first-relative-product A A' α B f (σB' t)) ( \ t → f (τB t)) ( \ t → homotopy-relative-product A A' α B f (σB' t))) : relative-extension-type I ψ ϕ - ( relative-product A A' α B f) ( B) - ( second-relative-product A A' α B f) + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) ( σB') ( τB) := ( \ t → ( (τA' t, τB t) , hA t) @@ -543,10 +563,10 @@ is equivalent to a generalized extension type for `A' → A`. #def general-relative-extension-type-relative-extension-type-pullback ( (τB', hB) : relative-extension-type I ψ ϕ - ( relative-product A A' α B f) ( B) - ( second-relative-product A A' α B f) + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) ( σB') ( τB)) - : general-relative-extension-type I ψ ϕ A' A α + : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) ( \ t → first-relative-product A A' α B f (σB' t)) ( \ t → f (τB t)) ( \ t → homotopy-relative-product A A' α B f (σB' t)) @@ -563,7 +583,6 @@ is equivalent to a generalized extension type for `A' → A`. ( τB t) ( f) ( hB t))) - #end relative-extension-type-pullback From c6c9ddfef6babcfe58868e379859ce3a7e99c24d Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 01:02:43 +0200 Subject: [PATCH 06/14] prove that right orthogonal maps are preserved under pullback --- .../04-right-orthogonal.rzk.md | 189 ++++++++++++++---- 1 file changed, 151 insertions(+), 38 deletions(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index c6641092..7c44ffb7 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -75,15 +75,22 @@ in terms of the contractibility of _relative extension types_. Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl] +#def relative-extension-type' + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + : U + := + fib + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + ( \ τ' t → α t (τ' t)) + ( τ) + #def equiv-relative-extension-type-fib uses (extext) ( σ' : (t : ϕ) → A' t) ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) : Equiv - ( fib - ( (t : ψ) → A' t [ϕ t ↦ σ' t]) - ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - ( \ τ' t → α t (τ' t)) - ( τ)) + ( relative-extension-type' σ' τ) ( relative-extension-type σ' τ) := total-equiv-family-equiv @@ -177,30 +184,7 @@ then also all generalized ones. #variables A' A : U #variable α : A' → A - -#def has-contr-relative-extension-types-is-right-orthogonal uses (extext) - ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) - : has-contr-relative-extension-types I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) - := - \ σ' τ → - is-contr-equiv-is-contr - ( fib - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( τ)) - ( relative-extension-type I ψ ϕ - ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) - ( equiv-relative-extension-type-fib I ψ ϕ - ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) - ( is-contr-map-is-equiv - ( (t : ψ) → A' [ϕ t ↦ σ' t]) - ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t)) - ( is-orth-α σ') - ( τ)) - -#def is-right-orthogonal-has-contr-relative-extension-types uses (extext) +#def is-right-orthogonal-to-shape-has-contr-relative-extension-types uses (extext) ( are-contr-relext-α : has-contr-relative-extension-types I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α)) @@ -225,6 +209,43 @@ then also all generalized ones. ( are-contr-relext-α σ' τ) ) +#def has-contr-relative-extension-types-is-right-orthogonal-to-shape uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-contr-relative-extension-types I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + := + \ σ' τ → + is-contr-equiv-is-contr + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( equiv-relative-extension-type-fib I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( is-contr-map-is-equiv + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( is-orth-α σ') + ( τ)) + +#def has-contr-general-relative-extension-types-is-right-orthogonal-to-shape + uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : ( σ' : (t : ϕ) → A') + → ( τ : (t : ψ) → A) + → ( h : (t : ϕ) → α (σ' t) = τ t) + → is-contr + ( general-relative-extension-type + I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) σ' τ h) + := + ( has-contr-relative-extension-types-generalize + I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)) + ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) + + #end has-contr-relative-extension-types-iff-is-right-orthogonal ``` @@ -533,20 +554,19 @@ More precisely: If `α : A' → A` is right orthogonal, then so is the second projection `relative-product A A' α B f → B` for every `f : B → A`. -To prove this, we show that each relative extension type +To prove this, we first show that each relative extension type of `relative-product A A' α B f → B`, -is equivalent to a generalized extension type for `A' → A`. +is a retract of a generalized extension type for `A' → A`. +Since the latter are all contractible by assumption, +the same follows for the former. ```rzk #variable B : U #variable f : B → A -#section relative-extension-type-pullback - -#variable σB' : ϕ → relative-product A A' α B f -#variable τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)] - #def relative-extension-type-pullback-general-relative-extension-type + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) ( (τA', hA) : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) ( \ t → first-relative-product A A' α B f (σB' t)) @@ -561,6 +581,8 @@ is equivalent to a generalized extension type for `A' → A`. , \ t → refl) #def general-relative-extension-type-relative-extension-type-pullback + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) ( (τB', hB) : relative-extension-type I ψ ϕ ( \ _ → relative-product A A' α B f) ( \ _ → B) @@ -583,10 +605,101 @@ is equivalent to a generalized extension type for `A' → A`. ( τB t) ( f) ( hB t))) -#end relative-extension-type-pullback - +#def is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb uses (extext) + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + : ( τhB + : relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + → ( relative-extension-type-pullback-general-relative-extension-type σB' τB + ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB) + = τhB) + := + ind-has-section-equiv + ( relative-extension-type' I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( equiv-relative-extension-type-fib I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( \ τhB → + ( relative-extension-type-pullback-general-relative-extension-type σB' τB + ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB) + = τhB)) + ( ind-fib + ( (t : ψ) → relative-product A A' α B f [ϕ t ↦ σB' t]) + ( (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + ( \ τB' t → second-relative-product A A' α B f (τB' t)) + ( \ τB₁ (τB'₁, h₁) → + ( relative-extension-type-pullback-general-relative-extension-type σB' τB₁ + ( general-relative-extension-type-relative-extension-type-pullback σB' τB₁ + ( τB'₁ + , ext-htpy-eq I ψ ϕ (\ _ → B) + ( \ t → second-relative-product A A' α B f (σB' t)) + ( \ t → second-relative-product A A' α B f (τB'₁ t)) + ( τB₁) ( h₁))) + = ( τB'₁ + , ext-htpy-eq I ψ ϕ (\ _ → B) + ( \ t → second-relative-product A A' α B f (σB' t)) + ( \ t → second-relative-product A A' α B f (τB'₁ t)) + ( τB₁) ( h₁)))) + ( \ τB' → refl) + ( τB)) + +#def is-retract-of-rel-ext-type-pb-gen-rel-ext-type uses (extext) + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + : is-retract-of + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + := + ( general-relative-extension-type-relative-extension-type-pullback σB' τB + , ( relative-extension-type-pullback-general-relative-extension-type σB' τB + , is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb σB' τB)) +``` +Then we can deduce that right orthogonal maps are preserved under pullback: +```rzk +#def is-right-orthoponal-pullback-to-shape uses (extext is-orth-ψ-ϕ-α) + : is-right-orthogonal-to-shape I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + := + is-right-orthogonal-to-shape-has-contr-relative-extension-types I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + ( \ σB' τB → + is-contr-is-retract-of-is-contr + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + ( is-retract-of-rel-ext-type-pb-gen-rel-ext-type σB' τB) + ( has-contr-general-relative-extension-types-is-right-orthogonal-to-shape + I ψ ϕ A' A α + ( is-orth-ψ-ϕ-α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t)))) #end right-orthogonal-calculus ``` From 874e02a85133982443fc4aa1e8ab0ec152219b1b Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 10:54:34 +0200 Subject: [PATCH 07/14] restructure and cleanup --- src/simplicial-hott/03-extension-types.rzk.md | 140 +++++++++++++++++ .../04-right-orthogonal.rzk.md | 142 ++---------------- 2 files changed, 150 insertions(+), 132 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 51b3ddeb..2b833e25 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -1111,3 +1111,143 @@ Using `ExtExt` we can write the homotopy in the homotopy extension type pointwis #end pointwise-homotopy-extension-type ``` + +## Relative extension types + +Given a map `α : A' → A`, there is also a notion of relative extension types. + +```rzk +#section relative-extension-types + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : ψ → U +#variable α : (t : ψ) → A' t → A t +#variable σ' : (t : ϕ) → A' t +#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)] + +#def relative-extension-type + : U + := + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl] + +#def relative-extension-type' + : U + := + fib + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + ( \ τ' t → α t (τ' t)) + ( τ) + +#def equiv-relative-extension-type-fib uses (extext) + : Equiv + ( relative-extension-type') + ( relative-extension-type) + := + total-equiv-family-equiv + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ) + ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) + ( \ τ' → + equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t)) + ( \ t → α t (τ' t)) ( τ)) +#end relative-extension-types +``` + +### Generalized relative extension types + +We will also need to allow more general relative extension types, +where we start with a `τ : ψ → A` that does not strictly restrict to +`\ t → α (σ' t)`. + +```rzk +#section general-extension-types + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : ψ → U +#variable α : (t : ψ) → A' t → A t + +#def general-relative-extension-type + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) + : U + := + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] +``` + +If all ordinary relative extension types are contractible, +then also all generalized ones. + +```rzk +#def has-contr-relative-extension-types + : U + := + ( σ' : (t : ϕ) → A' t) + → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)) + +#def has-contr-general-relative-extension-types + : U + := + ( σ' : (t : ϕ) → A' t) + → ( τ : (t : ψ) → A t) + → ( h : (t : ϕ) → α t (σ' t) = τ t) + → ( is-contr ( general-relative-extension-type σ' τ h)) + +#def has-contr-relative-extension-types-generalize' uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) + : is-contr + ( general-relative-extension-type σ' τ + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))) + := + ind-has-section-equiv + ( extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( extension-type-pointwise-weakening I ψ ϕ A (\ t → α t (σ' t))) + ( \ (τ̂ , ĥ) → + is-contr + ( general-relative-extension-type σ' τ̂ + ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t)))) + ( \ τ → has-contr-relext-α σ' τ) + ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t))) + +#def has-contr-relative-extension-types-generalize uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + : has-contr-general-relative-extension-types + := + \ σ' τ h → + transport + ( (t : ϕ) → α t (σ' t) = τ t) + ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ)) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) + ( h) + ( naiveextext-extext extext + ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) + ( h) + ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t))) + ( has-contr-relative-extension-types-generalize' + has-contr-relext-α σ' τ h) +``` + +The converse is of course trivial. + +```rzk +#def has-contr-relative-extension-types-specialize + ( has-contr-gen-relext-α : has-contr-general-relative-extension-types) + : has-contr-relative-extension-types + := + \ σ' τ → has-contr-gen-relext-α σ' τ (\ _ → refl) + +#end general-extension-types +``` diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 7c44ffb7..aa822c63 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -53,127 +53,11 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) ) ``` -## Relative extension types +## Contractible relative extension types Using `ExtExt`, we can characterize right orthogonal maps -in terms of the contractibility of _relative extension types_. - -```rzk -#section relative-extension-types - -#variable I : CUBE -#variable ψ : I → TOPE -#variable ϕ : ψ → TOPE -#variables A' A : ψ → U -#variable α : (t : ψ) → A' t → A t - -#def relative-extension-type - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - : U - := - Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) - , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl] - -#def relative-extension-type' - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - : U - := - fib - ( (t : ψ) → A' t [ϕ t ↦ σ' t]) - ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - ( \ τ' t → α t (τ' t)) - ( τ) - -#def equiv-relative-extension-type-fib uses (extext) - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - : Equiv - ( relative-extension-type' σ' τ) - ( relative-extension-type σ' τ) - := - total-equiv-family-equiv - ( (t : ψ) → A' t [ϕ t ↦ σ' t]) - ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ) - ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) - ( \ τ' → - equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t)) - ( \ t → α t (τ' t)) ( τ)) - -#def has-contr-relative-extension-types - : U - := - ( σ' : (t : ϕ) → A' t) - → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - → ( is-contr (relative-extension-type σ' τ)) -``` - -### Generalized relative extension types - -We will also need to allow more general relative extension types, -where we start with a `τ : ψ → A` that does not strictly restrict to -`\ t → α (σ' t)`. - -```rzk -#def general-relative-extension-type - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t) - ( h : (t : ϕ) → α t (σ' t) = τ t) - : U - := - Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) - , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] -``` - -If all ordinary relative extension types are contractible, -then also all generalized ones. - -```rzk -#def has-contr-relative-extension-types-generalize' uses (extext) - ( has-contr-relext-α : has-contr-relative-extension-types) - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t) - ( h : (t : ϕ) → α t (σ' t) = τ t) - : is-contr - ( general-relative-extension-type σ' τ - ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))) - := - ind-has-section-equiv - ( extension-type I ψ ϕ A (\ t → α t (σ' t))) - ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t))) - ( extension-type-pointwise-weakening extext I ψ ϕ A (\ t → α t (σ' t))) - ( \ (τ̂ , ĥ) → - is-contr - ( general-relative-extension-type σ' τ̂ - ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t)))) - ( \ τ → has-contr-relext-α σ' τ) - ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t))) - -#def has-contr-relative-extension-types-generalize uses (extext) - ( has-contr-relext-α : has-contr-relative-extension-types) - ( σ' : (t : ϕ) → A' t) - ( τ : (t : ψ) → A t) - ( h : (t : ϕ) → α t (σ' t) = τ t) - : is-contr ( general-relative-extension-type σ' τ h) - := - transport - ( (t : ϕ) → α t (σ' t) = τ t) - ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ)) - ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) - ( h) - ( naiveextext-extext extext - ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT) - ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) - ( h) - ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t))) - ( has-contr-relative-extension-types-generalize' - has-contr-relext-α σ' τ h) - -#end relative-extension-types -``` - -### Characterization of right orthogonality +in terms of the contractibility of relative extension types +or, equivalently, generalized extension types. ```rzk #section has-contr-relative-extension-types-iff-is-right-orthogonal @@ -204,7 +88,7 @@ then also all generalized ones. ( τ)) ( relative-extension-type I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) - ( equiv-relative-extension-type-fib I ψ ϕ + ( equiv-relative-extension-type-fib extext I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) ( are-contr-relext-α σ' τ) ) @@ -222,7 +106,7 @@ then also all generalized ones. ( τ)) ( relative-extension-type I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) - ( equiv-relative-extension-type-fib I ψ ϕ + ( equiv-relative-extension-type-fib extext I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) ( is-contr-map-is-equiv ( (t : ψ) → A' [ϕ t ↦ σ' t]) @@ -234,18 +118,13 @@ then also all generalized ones. #def has-contr-general-relative-extension-types-is-right-orthogonal-to-shape uses (extext) ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) - : ( σ' : (t : ϕ) → A') - → ( τ : (t : ψ) → A) - → ( h : (t : ϕ) → α (σ' t) = τ t) - → is-contr - ( general-relative-extension-type - I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) σ' τ h) + : has-contr-general-relative-extension-types I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) := - ( has-contr-relative-extension-types-generalize - I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)) + has-contr-relative-extension-types-generalize extext I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) - #end has-contr-relative-extension-types-iff-is-right-orthogonal ``` @@ -272,7 +151,6 @@ conditions. #variable is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α #variable is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α - -- rzk does not accept these terms after η-reduction ``` Using the vertical pasting calculus for homotopy cartesian squares, it is not @@ -626,7 +504,7 @@ the same follows for the former. ( \ _ → relative-product A A' α B f) ( \ _ → B) ( \ _ → second-relative-product A A' α B f) ( σB') ( τB)) - ( equiv-relative-extension-type-fib I ψ ϕ + ( equiv-relative-extension-type-fib extext I ψ ϕ ( \ _ → relative-product A A' α B f) ( \ _ → B) ( \ _ → second-relative-product A A' α B f) ( σB') ( τB)) From b2da8259e4e3633048761db57d3346071a9a30ff Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 10:58:48 +0200 Subject: [PATCH 08/14] autoformat documents --- src/simplicial-hott/03-extension-types.rzk.md | 12 +++++----- .../04-right-orthogonal.rzk.md | 22 +++++++++---------- 2 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 2b833e25..c9abd137 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -1066,7 +1066,8 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r ### Pointwise homotopy extension types -Using `ExtExt` we can write the homotopy in the homotopy extension type pointwise. +Using `ExtExt` we can write the homotopy in the homotopy extension type +pointwise. ```rzk #section pointwise-homotopy-extension-type @@ -1159,9 +1160,8 @@ Given a map `α : A' → A`, there is also a notion of relative extension types. ### Generalized relative extension types -We will also need to allow more general relative extension types, -where we start with a `τ : ψ → A` that does not strictly restrict to -`\ t → α (σ' t)`. +We will also need to allow more general relative extension types, where we start +with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`. ```rzk #section general-extension-types @@ -1182,8 +1182,8 @@ where we start with a `τ : ψ → A` that does not strictly restrict to , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] ``` -If all ordinary relative extension types are contractible, -then also all generalized ones. +If all ordinary relative extension types are contractible, then also all +generalized ones. ```rzk #def has-contr-relative-extension-types diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index aa822c63..7a7d53b2 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -41,7 +41,7 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ```rzk title="BW23, Section 3" #def is-right-orthogonal-to-shape ( I : CUBE) - ( ψ : I → TOPE ) + ( ψ : I → TOPE) ( ϕ : ψ → TOPE) ( A' A : U) ( α : A' → A) @@ -55,9 +55,9 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ## Contractible relative extension types -Using `ExtExt`, we can characterize right orthogonal maps -in terms of the contractibility of relative extension types -or, equivalently, generalized extension types. +Using `ExtExt`, we can characterize right orthogonal maps in terms of the +contractibility of relative extension types or, equivalently, generalized +extension types. ```rzk #section has-contr-relative-extension-types-iff-is-right-orthogonal @@ -427,16 +427,14 @@ stability properties of maps right orthogonal to it. ### Stability under pullback -Right orthogonal maps are stable under pullback. -More precisely: If `α : A' → A` is right orthogonal, -then so is the second projection +Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A` +is right orthogonal, then so is the second projection `relative-product A A' α B f → B` for every `f : B → A`. -To prove this, we first show that each relative extension type -of `relative-product A A' α B f → B`, -is a retract of a generalized extension type for `A' → A`. -Since the latter are all contractible by assumption, -the same follows for the former. +To prove this, we first show that each relative extension type of +`relative-product A A' α B f → B`, is a retract of a generalized extension type +for `A' → A`. Since the latter are all contractible by assumption, the same +follows for the former. ```rzk #variable B : U From ea0ce86ab0f1dbb291aced7b21929fa2776f3503 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 20:24:33 +0200 Subject: [PATCH 09/14] formatting edits --- src/hott/03-equivalences.rzk.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 36b391cd..451cc317 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -230,11 +230,11 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than ( f : A → B) ( ( sec-f , ε-f) : has-section A B f) ( C : B → U) - ( s : ( a : A) → C ( f a)) + ( s : (a : A) → C (f a)) ( b : B) : C b := - transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b)) + transport B C (f (sec-f b)) b (ε-f b) (s (sec-f b)) ``` It is convenient to have available the special case where `f` is an equivalence. @@ -243,7 +243,7 @@ It is convenient to have available the special case where `f` is an equivalence. #def ind-has-section-equiv ( A B : U) ( (f, is-equiv-f) : Equiv A B) - : ( C : B → U) → (( a : A) → C ( f a)) → ( b : B) → C b + : ( C : B → U) → ((a : A) → C (f a)) → (b : B) → C b := ind-has-section A B f (second is-equiv-f) ``` @@ -428,7 +428,7 @@ retraction the first map is an equivalence, and dually. ( ( comp C A B f retr-gf , ind-has-section A B f has-section-f ( \ b → f (retr-gf (g b)) = b) - ( \ a → ap A B (retr-gf (g ( f a))) a f (η-gf a)) + ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a)) ) , ( comp C A B f sec-gf, ε-gf) ) From 6d24a94de18f198baba3aa12ab534e2d26c20231 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 20:26:36 +0200 Subject: [PATCH 10/14] formatting edits --- src/hott/03-equivalences.rzk.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 451cc317..83c9613e 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -233,8 +233,7 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than ( s : (a : A) → C (f a)) ( b : B) : C b - := - transport B C (f (sec-f b)) b (ε-f b) (s (sec-f b)) + := transport B C (f (sec-f b)) b (ε-f b) (s (sec-f b)) ``` It is convenient to have available the special case where `f` is an equivalence. @@ -244,8 +243,7 @@ It is convenient to have available the special case where `f` is an equivalence. ( A B : U) ( (f, is-equiv-f) : Equiv A B) : ( C : B → U) → ((a : A) → C (f a)) → (b : B) → C b - := - ind-has-section A B f (second is-equiv-f) + := ind-has-section A B f (second is-equiv-f) ``` ## Composing equivalences From 777e482f8b82821d44545e866f218240cb4ff0e3 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 20:30:51 +0200 Subject: [PATCH 11/14] formatting changes --- src/hott/03-equivalences.rzk.md | 90 +++++++++++++++------------------ 1 file changed, 40 insertions(+), 50 deletions(-) diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 83c9613e..55cc7383 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -404,14 +404,12 @@ retraction the first map is an equivalence, and dually. ( ( (retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f)) : is-equiv A B f := - ( ( comp B C A retr-gf g, η-gf) , - ( comp B C A sec-gf g , - \ b → + ( ( comp B C A retr-gf g, η-gf) + , ( comp B C A sec-gf g + , \ b → ap-cancel-has-retraction B C g has-retraction-g (f (sec-gf (g b))) b - ( ε-gf (g b)) - ) - ) + ( ε-gf (g b)))) ``` ```rzk title="Left cancellation of equivalence property in diagrammatic order" @@ -426,10 +424,8 @@ retraction the first map is an equivalence, and dually. ( ( comp C A B f retr-gf , ind-has-section A B f has-section-f ( \ b → f (retr-gf (g b)) = b) - ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a)) - ) , - ( comp C A B f sec-gf, ε-gf) - ) + ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a))) + , ( comp C A B f sec-gf, ε-gf)) ``` We typically apply the cancelation property in a setting where the composite and @@ -496,16 +492,16 @@ If a map is homotopic to an equivalence it is an equivalence. ( is-equiv-g : is-equiv A B g) : is-equiv A B f := - ( ( ( first (first is-equiv-g)) , - ( \ a → + ( ( ( first (first is-equiv-g)) + , ( \ a → concat A ( first (first is-equiv-g) (f a)) ( first (first is-equiv-g) (g a)) ( a) ( ap B A (f a) (g a) (first (first is-equiv-g)) (H a)) - ( second (first is-equiv-g) a))) , - ( ( first (second is-equiv-g)) , - ( \ b → + ( second (first is-equiv-g) a))) + , ( ( first (second is-equiv-g)) + , ( \ b → concat B ( f (first (second is-equiv-g) b)) ( g (first (second is-equiv-g) b)) @@ -633,8 +629,8 @@ dependent function types. ( famisequiv : (x : X) → is-equiv (A x) (B x) (f x)) : is-equiv ((x : X) → A x) ((x : X) → B x) ( \ a x → f x (a x)) := - ( ( ( \ b x → first (first (famisequiv x)) (b x)) , - ( \ a → + ( ( ( \ b x → first (first (famisequiv x)) (b x)) + , ( \ a → eq-htpy X A ( \ x → @@ -642,13 +638,12 @@ dependent function types. ( first (famisequiv x)) ( f x (a x))) ( a) - ( \ x → second (first (famisequiv x)) (a x)))) , - ( ( \ b x → first (second (famisequiv x)) (b x)) , - ( \ b → + ( \ x → second (first (famisequiv x)) (a x)))) + , ( ( \ b x → first (second (famisequiv x)) (b x)) + , ( \ b → eq-htpy X B - ( \ x → - f x (first (second (famisequiv x)) (b x))) + ( \ x → f x (first (second (famisequiv x)) (b x))) ( b) ( \ x → second (second (famisequiv x)) (b x))))) ``` @@ -660,8 +655,8 @@ dependent function types. ( famequiv : (x : X) → Equiv (A x) (B x)) : Equiv ((x : X) → A x) ((x : X) → B x) := - ( ( \ a x → (first (famequiv x)) (a x)) , - ( is-equiv-function-is-equiv-family + ( ( \ a x → (first (famequiv x)) (a x)) + , ( is-equiv-function-is-equiv-family ( X) ( A) ( B) @@ -729,20 +724,20 @@ dependent function types. ( p : x = y) : Equiv (y = z) (x = z) := - ( concat A x y z p, - ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p), - ( concat A y x z (rev A x y p), section-preconcat A x y z p))) + ( concat A x y z p + , ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p) + , ( concat A y x z (rev A x y p), section-preconcat A x y z p))) #def equiv-postconcat ( A : U) ( x y z : A) ( q : y = z) : Equiv (x = y) (x = z) := - ( \ p → concat A x y z p q, - ( ( \ r → concat A x z y r (rev A y z q), - retraction-postconcat A x y z q), - ( \ r → concat A x z y r (rev A y z q), - section-postconcat A x y z q))) + ( \ p → concat A x y z p q + , ( ( \ r → concat A x z y r (rev A y z q) + , retraction-postconcat A x y z q) + , ( \ r → concat A x z y r (rev A y z q) + , section-postconcat A x y z q))) ``` ## Transport along a path is an equivalence @@ -768,8 +763,8 @@ dependent function types. ( β : B' → B) : U := - Σ ( ( s',s) : product ( A' → B' ) ( A → B)), - ( ( a' : A') → β ( s' a') = s ( α a')) + Σ ( ( s',s) : product ( A' → B' ) ( A → B)) + , ( ( a' : A') → β ( s' a') = s ( α a')) #def Equiv-of-maps ( A' A : U) @@ -778,11 +773,10 @@ dependent function types. ( β : B' → B) : U := - Σ ( ((s', s), _) : map-of-maps A' A α B' B β), - ( product - ( is-equiv A' B' s') - ( is-equiv A B s) - ) + Σ ( ((s', s), _) : map-of-maps A' A α B' B β) + , ( product + ( is-equiv A' B' s') + ( is-equiv A B s)) #def is-equiv-equiv-is-equiv ( A' A : U) @@ -797,11 +791,10 @@ dependent function types. := is-equiv-right-factor A' A B α s is-equiv-s ( is-equiv-rev-homotopy A' B - ( comp A' B' B β s') - ( comp A' A B s α) - ( η ) - ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β) - ) + ( comp A' B' B β s') + ( comp A' A B s α) + ( η ) + ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β)) #def is-equiv-Equiv-is-equiv ( A' A : U) @@ -810,8 +803,7 @@ dependent function types. ( β : B' → B) ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β ) : is-equiv B' B β → is-equiv A' A α - := - is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s + := is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s #def is-equiv-equiv-is-equiv' ( A' A : U) @@ -829,8 +821,7 @@ dependent function types. ( comp A' B' B β s') ( comp A' A B s α) ( η) - ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s) - ) + ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s)) #def is-equiv-Equiv-is-equiv' ( A' A : U) @@ -839,6 +830,5 @@ dependent function types. ( β : B' → B) ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β ) : is-equiv A' A α → is-equiv B' B β - := - is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s + := is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s ``` From e6bb318cd2eb6a68d48113582b8df2a399cf4246 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 17:16:53 +0200 Subject: [PATCH 12/14] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- src/hott/03-equivalences.rzk.md | 4 ++-- src/simplicial-hott/03-extension-types.rzk.md | 24 +++++++++---------- .../04-right-orthogonal.rzk.md | 3 +-- 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 55cc7383..6ffd6ddc 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -421,8 +421,8 @@ retraction the first map is an equivalence, and dually. ( ( ( retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f)) : is-equiv B C g := - ( ( comp C A B f retr-gf , - ind-has-section A B f has-section-f + ( ( comp C A B f retr-gf + , ind-has-section A B f has-section-f ( \ b → f (retr-gf (g b)) = b) ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a))) , ( comp C A B f sec-gf, ε-gf)) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index c9abd137..87dc12fc 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -70,8 +70,8 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of : has-section (extension-type σ) (homotopy-extension-type σ) (extension-type-weakening-map σ) := - ( extension-strictification σ, - \ th → ( second (section-extension-type-weakening' σ th))) + ( extension-strictification σ + , \ th → ( second (section-extension-type-weakening' σ th))) #def is-equiv-extension-type-weakening @@ -120,9 +120,7 @@ This equivalence is functorial in the following sense: , \ _ → refl ) , ( is-equiv-extension-type-weakening I ψ ϕ A' σ' - , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t)) - ) - ) + , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t)))) ``` ## Commutation of arguments and currying @@ -1095,7 +1093,7 @@ pointwise. ( \ τ → (t : ϕ) → (τ t = σ t)) ( \ τ → equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t) - ( \ _ → recBOT) ( \ t → τ t) ( σ)) + ( \ _ → recBOT) (\ t → τ t) σ) #def extension-type-pointwise-weakening uses (extext) ( σ : (t : ϕ) → A t) @@ -1132,7 +1130,7 @@ Given a map `α : A' → A`, there is also a notion of relative extension types. : U := Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) - , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl] + , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) #def relative-extension-type' : U @@ -1182,24 +1180,24 @@ with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`. , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] ``` -If all ordinary relative extension types are contractible, then also all -generalized ones. +If all ordinary relative extension types are contractible, then all +generalized extension types are also contractible. ```rzk #def has-contr-relative-extension-types : U := - ( σ' : (t : ϕ) → A' t) + ( ( σ' : (t : ϕ) → A' t) → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)) + → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ))) #def has-contr-general-relative-extension-types : U := - ( σ' : (t : ϕ) → A' t) + ( ( σ' : (t : ϕ) → A' t) → ( τ : (t : ψ) → A t) → ( h : (t : ϕ) → α t (σ' t) = τ t) - → ( is-contr ( general-relative-extension-type σ' τ h)) + → ( is-contr ( general-relative-extension-type σ' τ h))) #def has-contr-relative-extension-types-generalize' uses (extext) ( has-contr-relext-α : has-contr-relative-extension-types) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 7a7d53b2..bf4dae32 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -90,8 +90,7 @@ extension types. ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) ( equiv-relative-extension-type-fib extext I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) - ( are-contr-relext-α σ' τ) - ) + ( are-contr-relext-α σ' τ)) #def has-contr-relative-extension-types-is-right-orthogonal-to-shape uses (extext) ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) From fc9b9117582494fe4f2375d87b71d082d7f89739 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 17:43:38 +0200 Subject: [PATCH 13/14] autoformat --- src/simplicial-hott/03-extension-types.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 87dc12fc..0e0553e3 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -1180,8 +1180,8 @@ with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`. , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] ``` -If all ordinary relative extension types are contractible, then all -generalized extension types are also contractible. +If all ordinary relative extension types are contractible, then all generalized +extension types are also contractible. ```rzk #def has-contr-relative-extension-types From e65b13a173a5e9196b6420300c6f3c6e912a14e6 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 21:04:00 +0200 Subject: [PATCH 14/14] Update src/simplicial-hott/04-right-orthogonal.rzk.md Co-authored-by: Fredrik Bakke --- src/simplicial-hott/04-right-orthogonal.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 95a5551e..a170619f 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -123,7 +123,7 @@ extension types. := has-contr-relative-extension-types-generalize extext I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) - ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) + ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) #end has-contr-relative-extension-types-iff-is-right-orthogonal ```