From f4e6d4a5228f1c3552b2b2acecebf00e24cd28c7 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 9 Nov 2023 22:52:58 +0100 Subject: [PATCH 1/3] functorian isomorphisms --- src/hott/11-homotopy-pullbacks.rzk.md | 116 ++++++++++++++++++ .../02-simplicial-type-theory.rzk.md | 91 ++++++++++++++ .../04-right-orthogonal.rzk.md | 76 +++++++++++- src/simplicial-hott/08-covariant.rzk.md | 2 - 4 files changed, 277 insertions(+), 8 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index a2d6c5c6..3c67c9c9 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -240,6 +240,7 @@ maps `β → α` and obtain another homotopy cartesian square. ( is-equiv-transport A C (α (s' b')) (s (β b')) (η b')) ``` + ## Pasting calculus for homotopy cartesian squares Currently our notion of squares is not symmetric, since the vertical maps are @@ -247,6 +248,8 @@ given by type families, i.e. they are _display maps_, while the horizontal maps are arbitrary. Therefore we distinquish between the vertical and the horizontal pasting calculus. + + ### Vertical calculus The following vertical composition and cancellation laws follow easily from the @@ -472,6 +475,119 @@ In fact, it suffices to assume that the left square has horizontal sections. #end homotopy-cartesian-horizontal-calculus ``` +### Homotopy cartesian faces of a cube + +Consider two squares induced by type families as follows + +```rzk +#section is-homotopy-cartesian-in-cube + +#variable A' : U +#variable C' : A' → U +#variable A : U +#variable C : A → U +#variable α : A' → A +#variable γ : (a' : A') → C' a' → C (α a') + +#variable B' : U +#variable D' : B' → U +#variable B : U +#variable D : B → U +#variable β : B' → B +#variable δ : (b' : B') → D' b' → D (β b') +``` + +and a map between them in the following strict sense + +```rzk +#variable f' : A' → B' +#variable f : A → B +#variable h : (a' : A') → β (f' a') = f (α a') + +#variable F' : (a' : A') → C' a' → D' (f' a') +#variable F : (a : A) → C a → D (f a) +#variable H + : (a' : A') + → (c' : C' a') + → ( transport B D (β (f' a')) (f (α a')) (h a') + ( δ (f' a') (F' a' c')) + = F (α a') (γ a' c')) +``` + +We view this as a cube + +``` + Σ D' Σ D + +Σ C' Σ C + + B' B + + A' A +``` + +with display maps going down and ordinary maps going to the right and up-right. + +Assume furthermore that the two squares on the left and right are themselves +homotopy cartesian. + +```rzk +#variable is-hc-CD' : is-homotopy-cartesian A' C' B' D' f' F' +#variable is-hc-CD : is-homotopy-cartesian A C B D f F +``` + +If the square `B' D' B D` is homotopy cartesian, then so is `A' C' A C`. + +```rzk +#def is-homotopy-cartesian-in-cube + : is-homotopy-cartesian B' D' B D β δ + → is-homotopy-cartesian A' C' A C α γ + := + \ is-hc-BD a' → + is-equiv-equiv-is-equiv + ( C' a') (C (α a')) (γ a') + ( D' (f' a')) (D (f (α a'))) + (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d')) + ( ( F' a' , F (α a')) , H a') + ( is-hc-CD' a') + ( is-hc-CD (α a')) + ( is-equiv-comp + ( D' (f' a')) (D (β (f' a'))) (D (f (α a'))) + ( δ (f' a')) (is-hc-BD (f' a')) + ( transport B D (β (f' a')) (f (α a')) (h a')) + ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a'))) +``` + +The converse holds provided that the map `f' : A' → B'` has a section. + +```rzk +#def is-homotopy-cartesian-in-cube' + ( has-sec-f' : has-section A' B' f') + : is-homotopy-cartesian A' C' A C α γ + → is-homotopy-cartesian B' D' B D β δ + := + \ is-hc-AC → + ind-has-section A' B' f' has-sec-f' + ( \ b' → is-equiv (D' b') (D (β b')) (δ b')) + ( \ a' → + ( is-equiv-right-factor + ( D' (f' a')) (D (β (f' a'))) (D (f (α a'))) + ( δ (f' a')) + ( transport B D (β (f' a')) (f (α a')) (h a')) + ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a')) + ( is-equiv-equiv-is-equiv' + ( C' a') (C (α a')) (γ a') + ( D' (f' a')) (D (f (α a'))) + (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d')) + ( ( F' a' , F (α a')) , H a') + ( is-hc-CD' a') + ( is-hc-CD (α a')) + ( is-hc-AC a')))) + +#end is-homotopy-cartesian-in-cube +``` + + ## Fiber products Given two type families `B C : A → U`, we can form their **fiberwise product**. diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md index 24c1d77a..5feded51 100644 --- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md +++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md @@ -334,3 +334,94 @@ to diagrams extending a fixed diagram `σ': ϕ → A'` (or, respectively, its im , \ τ' → second (is-fretract-ψ-χ A' A α) τ' ) ``` + +### Isomorphisms of shape inclusions + +Consider two shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ`. We want to express the fact +that there is an isomorphism `ψ ≅ χ` of shapes which restricts to an isomorphism +`ϕ ≅ ζ`. Since shapes are not types themselves, the best we can currently do is +describe this isomorphism on representables. + +```rzk +#def isomorphism-shape-inclusions + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( J : CUBE) + ( χ : J → TOPE) + ( ζ : χ → TOPE) + : U + := + ( Σ ( f + : (A : U) + → Equiv (ζ → A) (ϕ → A)) + , ( ( A : U) + → ( σ : ζ → A) + → ( Equiv + ( (t : χ) → A [ζ t ↦ σ t]) + ( (t : ψ) → A [ϕ t ↦ first (f A) σ t])))) + +#def functorial-isomorphism-shape-inclusions + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( J : CUBE) + ( χ : J → TOPE) + ( ζ : χ → TOPE) + : U + := + Σ ( (f , F) : isomorphism-shape-inclusions I ψ ϕ J χ ζ) + , ( Σ ( e + : ( A' : U) + → ( A : U) + → ( α : A' → A) + → ( σ' : ζ → A') + → ( ( \ (t : I | ϕ t) → α (first (f A') σ' t)) + = ( first (f A) (\ t → α (σ' t))))) + , ( ( A' : U) + → ( A : U) + → ( α : A' → A) + → ( σ' : ζ → A') + → ( τ' : (t : χ) → A' [ζ t ↦ σ' t]) + → ( ( transport (ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t]) + ( \ (t : I | ϕ t) → α (first (f A') σ' t)) + ( first (f A) (\ t → α (σ' t))) + ( e A' A α σ') + (\ (t : ψ) → α (first (F A' σ') τ' t))) + = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t)))))) +``` + +As an example, we show establish the canonical isomorphism between the pairs +`{0} ⊂ Δ¹` and `{1} ⊂ right-leg-of-Λ`. It really just boils down to the two +formulas `\ τ (t , s) → τ s` describing the map +`(Δ¹ → A) → (right-leg-of-Λ → A)` and `\ υ s → υ (1₂ , s)` describing its +inverse. All of the necessary coherences are just `refl`. Unfortunately, there +is currently no better way to define this functorial isomorphism other than +spelling out the following monstrosity: + +```rzk +#def right-leg-of-Λ : Λ → TOPE + := \ (t, s) → t ≡ 1₂ + +#def isomorphism-0-Δ¹-1-right-leg-of-Λ + : isomorphism-shape-inclusions + (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂) + 2 Δ¹ (\ t → t ≡ 0₂) + := + ( \ A → + ( \ τ (t,s) → τ s + , ( ( \ υ s → υ (1₂, s) , \ _ → refl) + , ( \ υ s → υ (1₂, s) , \ _ → refl))) + , \ A _ → + ( \ τ (t,s) → τ s + , ( ( \ υ s → υ (1₂, s) , \ _ → refl) + , ( \ υ s → υ (1₂, s) , \ _ → refl)))) + +#def functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ + : functorial-isomorphism-shape-inclusions + (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂) + 2 Δ¹ (\ t → t ≡ 0₂) + := + ( isomorphism-0-Δ¹-1-right-leg-of-Λ + , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl)) +``` diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index a572e002..e848442c 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -193,7 +193,7 @@ occasionally go back or forth along the functorial equivalence ( is-orth-ψ-ϕ σ')) ``` -### Stability under composition +### Composition Left orthogonal shape inclusions are preserved under composition. @@ -229,7 +229,7 @@ Left orthogonal shape inclusions are preserved under composition. σ') ``` -### Cancellation laws +### Cancellation If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`. @@ -319,7 +319,7 @@ affecting left orthogonality. ( is-orth-ψ-ϕ (\ (s , t) → σ' (t , s))) ``` -### Stability under exponentiation +### Exponentiation If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`. @@ -402,7 +402,7 @@ extensionality. ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ is-orth-ψ-ϕ) ``` -### Stability under exact pushouts +### Exact pushouts For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`, then so is `ψ ⊂ ϕ ∪ ψ`. @@ -482,6 +482,70 @@ stability under pushout products. ( is-orth-ψ-ϕ)) ``` +### Functorial isomorphisms of shape inclusion + +If two pairs of shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ` are isomorphic, then +`ϕ ⊂ ψ` is left orthogonal if and only if `ζ ⊂ χ` is left orthogonal. + +```rzk +#def is-right-orthogonal-to-shape-isomorphism' + ( A' A : U) + ( α : A' → A) + ( I : CUBE) + ( ψ : I → TOPE ) + ( ϕ : ψ → TOPE ) + ( J : CUBE) + ( χ : J → TOPE) + ( ζ : χ → TOPE) + ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + → is-right-orthogonal-to-shape J χ ζ A' A α + := + is-homotopy-cartesian-in-cube + ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t]) + ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( first (f A')) ( first (f A)) + ( e A' A α) + ( \ σ' → first (F A' σ')) (\ σ → first (F A σ)) + ( E A' A α) + ( \ σ' → second (F A' σ')) (\ σ → second (F A σ)) + +#def is-right-orthogonal-to-shape-isomorphism + ( A' A : U) + ( α : A' → A) + ( I : CUBE) + ( ψ : I → TOPE ) + ( ϕ : ψ → TOPE ) + ( J : CUBE) + ( χ : J → TOPE) + ( ζ : χ → TOPE) + ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ) + : is-right-orthogonal-to-shape J χ ζ A' A α + → is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-homotopy-cartesian-in-cube' + ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t]) + ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( first (f A')) ( first (f A)) + ( e A' A α) + ( \ σ' → first (F A' σ')) (\ σ → first (F A σ)) + ( E A' A α) + ( \ σ' → second (F A' σ')) (\ σ → second (F A σ)) + ( second (second (f A'))) +``` + ## Stability properties of right orthogonal maps Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate @@ -523,7 +587,7 @@ Right orthogonality is closed under homotopy. ( first (first (funext A' (\ _ → A) α β)) h) ``` -### Stability under composition +### Composition ```rzk #variables A'' A' A : U @@ -596,7 +660,7 @@ right (whether it is right orthogonal or not.) ( is-orth-ψ-ϕ-αα') ``` -### Stability under pullback +### Pullback Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A` is right orthogonal, then so is the second projection diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 0afb7daf..89889f5d 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -309,8 +309,6 @@ The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes `{1} ⊂ right-leg-of-Λ` of `Λ`. ```rzk -#def right-leg-of-Λ : Λ → TOPE - := \ (t, s) → t ≡ 1₂ #def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start ( B : U) From 3990b9c3814010a26161864cf5c9d00f1d660937 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 9 Nov 2023 23:07:52 +0100 Subject: [PATCH 2/3] improve exposition --- .../02-simplicial-type-theory.rzk.md | 36 +++++++++++++------ 1 file changed, 26 insertions(+), 10 deletions(-) diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md index 5feded51..0278b82f 100644 --- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md +++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md @@ -352,9 +352,7 @@ describe this isomorphism on representables. ( ζ : χ → TOPE) : U := - ( Σ ( f - : (A : U) - → Equiv (ζ → A) (ϕ → A)) + ( Σ ( f : (A : U) → Equiv (ζ → A) (ϕ → A)) , ( ( A : U) → ( σ : ζ → A) → ( Equiv @@ -391,17 +389,35 @@ describe this isomorphism on representables. = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t)))))) ``` -As an example, we show establish the canonical isomorphism between the pairs -`{0} ⊂ Δ¹` and `{1} ⊂ right-leg-of-Λ`. It really just boils down to the two -formulas `\ τ (t , s) → τ s` describing the map -`(Δ¹ → A) → (right-leg-of-Λ → A)` and `\ υ s → υ (1₂ , s)` describing its -inverse. All of the necessary coherences are just `refl`. Unfortunately, there -is currently no better way to define this functorial isomorphism other than -spelling out the following monstrosity: +In practice, the isomorphisms are usually given via an explicit formula, which +would define a map `ψ → ϕ` if `ψ` and `ϕ` were themselves types. In this case +all the coherences are just `refl`, hence it is easy to produce a term of type +`functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ`. + +For example, consider the two shape inclusions `{0} ⊂ Δ¹` (subshapes of `2`) and +`{1} ⊂ right-leg-of-Λ` (subshapes of `2 × 2`), where ```rzk #def right-leg-of-Λ : Λ → TOPE := \ (t, s) → t ≡ 1₂ +``` + +These two shape inclusions are canonically isomorphic via the formulas + +``` +-- not valid rzk code +#def f : Δ¹ → right-leg-of-Λ + \ s → (1₂ , s) + +#def g : right-leg-of-Λ → Δ¹ + \ (t , s) → s +``` + +We turn these formulas into a functorial shape inclusion as follows. +Unfortunately we have to repeat the same formula multiple times, leading to some +ugly boilerplate code. + +```rzk #def isomorphism-0-Δ¹-1-right-leg-of-Λ : isomorphism-shape-inclusions From ff675fc2be4469f2640c4e2ff05b1c122b688bac Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 9 Nov 2023 23:25:08 +0100 Subject: [PATCH 3/3] autoformat --- src/hott/11-homotopy-pullbacks.rzk.md | 4 ---- src/simplicial-hott/02-simplicial-type-theory.rzk.md | 1 - 2 files changed, 5 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 3c67c9c9..84b336c1 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -240,7 +240,6 @@ maps `β → α` and obtain another homotopy cartesian square. ( is-equiv-transport A C (α (s' b')) (s (β b')) (η b')) ``` - ## Pasting calculus for homotopy cartesian squares Currently our notion of squares is not symmetric, since the vertical maps are @@ -248,8 +247,6 @@ given by type families, i.e. they are _display maps_, while the horizontal maps are arbitrary. Therefore we distinquish between the vertical and the horizontal pasting calculus. - - ### Vertical calculus The following vertical composition and cancellation laws follow easily from the @@ -587,7 +584,6 @@ The converse holds provided that the map `f' : A' → B'` has a section. #end is-homotopy-cartesian-in-cube ``` - ## Fiber products Given two type families `B C : A → U`, we can form their **fiberwise product**. diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md index 0278b82f..973e5dab 100644 --- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md +++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md @@ -418,7 +418,6 @@ Unfortunately we have to repeat the same formula multiple times, leading to some ugly boilerplate code. ```rzk - #def isomorphism-0-Δ¹-1-right-leg-of-Λ : isomorphism-shape-inclusions (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)