diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md index 973e5dab..9797166d 100644 --- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md +++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md @@ -298,7 +298,7 @@ for a section of the family of extensions of a function `ϕ → A` to a function For example, this applies to `Δ² ⊂ Δ¹×Δ¹`. ```rzk -#def Δ²-is-functorial-retract-Δ¹×Δ¹ +#def is-functorial-retract-Δ²-Δ¹×Δ¹ : is-functorial-shape-retract (2 × 2) (Δ¹×Δ¹) (Δ²) := \ A' A α → diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 8accefa8..6033e515 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -12,7 +12,6 @@ Some of the definitions in this file rely on extension extensionality or function extensionality: ```rzk -#assume naiveextext : NaiveExtExt #assume extext : ExtExt #assume funext : FunExt ``` @@ -327,7 +326,7 @@ The following proof uses a lot of currying and uncurrying and relies extension extensionality. ```rzk -#def is-right-orthogonal-to-shape-product uses (naiveextext) +#def is-right-orthogonal-to-shape-product uses (extext) ( A' A : U) ( α : A' → A) ( J : CUBE) @@ -344,7 +343,7 @@ extensionality. ( t, s) → ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s , \ ( τ' : ( (t , s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t , s)]) → - naiveextext + naiveextext-extext extext ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s) ( \ _ → A') ( \ ( t,s) → σ' (t , s)) @@ -364,7 +363,7 @@ extensionality. ( t, s) → ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s , \ ( τ : ( (t , s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t , s))]) → - naiveextext + naiveextext-extext extext ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s) ( \ _ → A) ( \ (t , s) → α (σ' (t , s))) @@ -383,7 +382,7 @@ extensionality. ( \ s' → τ (t, s'))) ( s)))) -#def is-right-orthogonal-to-shape-product' uses (naiveextext) +#def is-right-orthogonal-to-shape-product' uses (extext) ( A' A : U) ( α : A' → A) ( I : CUBE) @@ -432,7 +431,7 @@ Combining the stability under pushouts and crossing with a shape, we get stability under pushout products. ```rzk -#def is-right-orthogonal-to-shape-pushout-product uses (naiveextext) +#def is-right-orthogonal-to-shape-pushout-product uses (extext) ( A' A : U) ( α : A' → A) ( J : CUBE) @@ -459,7 +458,7 @@ stability under pushout products. ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ ( is-orth-ψ-ϕ)) -#def is-right-orthogonal-to-shape-pushout-product' uses (naiveextext) +#def is-right-orthogonal-to-shape-pushout-product' uses (extext) ( A' A : U) ( α : A' → A) ( I : CUBE) @@ -1247,7 +1246,7 @@ conditions of being anodyne. ( is-right-orthogonal-to-shape-right-cancel-retract A' A α I ψ χ ϕ ( f A' A α is-orth₀) ( r)) -#def is-anodyne-pushout-product-for-shape uses (naiveextext) +#def is-anodyne-pushout-product-for-shape uses (extext) ( J : CUBE) ( χ : J → TOPE) ( ζ : χ → TOPE) @@ -1263,7 +1262,7 @@ conditions of being anodyne. ( is-right-orthogonal-to-shape-pushout-product A' A α J χ ζ I ψ ϕ ( f A' A α is-orth₀)) -#def is-anodyne-pushout-product-for-shape' uses (naiveextext) +#def is-anodyne-pushout-product-for-shape' uses (extext) ( I : CUBE) ( ψ : I → TOPE ) ( ϕ : ψ → TOPE ) @@ -1346,8 +1345,7 @@ analog fo weak anodyne shape inclusions. ( is-right-orthogonal-terminal-map-has-unique-extensions I ψ ϕ A has-ue-ψ-ϕ)) -#def is-weak-anodyne-pushout-product-for-shape - uses (naiveextext extext) +#def is-weak-anodyne-pushout-product-for-shape uses (extext) ( I : CUBE) ( ψ : I → TOPE ) ( ϕ : ψ → TOPE ) @@ -1367,8 +1365,7 @@ analog fo weak anodyne shape inclusions. is-right-orthogonal-to-shape-pushout-product A'₁ A₁ α₁ J χ ζ I ψ ϕ) ( A) (f A has-ue₀) -#def is-weak-anodyne-pushout-product-for-shape' - uses (naiveextext extext) +#def is-weak-anodyne-pushout-product-for-shape' uses (extext) ( I : CUBE) ( ψ : I → TOPE ) ( ϕ : ψ → TOPE ) diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index dc45bedf..904d40b2 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -1671,6 +1671,43 @@ Interchange law #end homotopy-interchange-law ``` +## Inner anodyne shape inclusions + +An **inner fibration** is a map `α : A' → A` which is right orthogonal to +`Λ ⊂ Δ²`. This is the relative notion of a Segal type. + +```rzk +#def is-inner-fibration + ( A' A : U) + ( α : A' → A) + : U + := is-right-orthogonal-to-shape (2 × 2) Δ² (\ t → Λ t) A' A α +``` + +We say that a shape inclusion `ϕ ⊂ ψ` is **inner anodyne** if it is anodyne for +`Λ ⊂ Δ²`, i.e., if every inner fibration `A' → A` is right orthogonal to +`ϕ ⊂ ψ`. + +```rzk +#def is-inner-anodyne + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + : U + := is-anodyne-for-shape (2 × 2) (Δ²) (\ t → Λ t) I ψ ϕ + +#def unpack-is-inner-anodyne + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + : is-inner-anodyne I ψ ϕ + = ( (A' : U) → (A : U) → (α : A' → A) + → is-inner-fibration A' A α + → is-right-orthogonal-to-shape I ψ ϕ A' A α) + := refl + +``` + ## Weak inner anodyne shape inclusions We say that a shape inclusion `ϕ ⊂ ψ` is **weak inner anodyne** if every Segal @@ -1871,19 +1908,6 @@ It should be easy to adapt it to prove that it is actually inner anodyne. ( h^ A h)) ``` -## Inner fibrations - -An inner fibration is a map `α : A' → A` which is right orthogonal to `Λ ⊂ Δ²`. -This is the relative notion of a Segal type. - -```rzk -#def is-inner-fibration - ( A' A : U) - ( α : A' → A) - : U - := is-right-orthogonal-to-shape (2 × 2) Δ² (\ t → Λ t) A' A α -``` - ## Products of Segal types This is an additional section which describes morphisms in products of types as diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index 67f0fe2d..2b419242 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -358,7 +358,181 @@ Every contractible type is automatically discrete. ## Discrete types are Segal types -Discrete types are automatically Segal types. +Recall that we can characterize discrete type either as those local for +`{0} ⊂ Δ¹` _or_, equivalently, as those that are local for `{1} ⊂ Δ¹`. This +suggests two different relative notions of discreteness and corresponding +notions of anodyne shape inclusions. + +Note that while the absolute notions of locality for `{0} ⊂ Δ¹` and `{1} ⊂ Δ¹` +agree, the relative notions _do not_. We will explore this discrepancy more when +we introduce covariant and contravariant type families. + +```rzk +#def is-left-fibration + ( A' A : U) + ( α : A' → A) + : U + := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α + +#def is-right-fibration + ( A' A : U) + ( α : A' → A) + : U + := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 1₂) A' A α +``` + +### Left and right anodyne shape inclusions + +```rzk +#def is-left-anodyne + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + : U + := is-anodyne-for-shape 2 Δ¹ ( \ s → s ≡ 0₂) I ψ ϕ + +#def is-right-anodyne + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + : U + := is-anodyne-for-shape 2 Δ¹ ( \ s → s ≡ 1₂) I ψ ϕ +``` + +### Left fibrations are inner fibrations + +We aim to show that every left fibration is an inner fibration, i.e. that the +inner horn inclusion `Λ ⊂ Δ²` is left anodyne. + +The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes +`{1} ⊂ right-leg-of-Λ` of `Λ`. + +```rzk +#def is-left-anodyne-1-right-leg-of-Λ + : is-left-anodyne ( 2 × 2) + (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂) + := + \ A' A α → + is-right-orthogonal-to-shape-isomorphism A' A α + ( 2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂) + ( 2) (Δ¹) (\ t → t ≡ 0₂) + ( functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ) +``` + +Next we use that `Λ` is the pushout of its left leg and its right leg to deduce +that the pair `left-leg-of-Λ ⊂ Λ` is left anodyne. + +```rzk +#def left-leg-of-Λ : Λ → TOPE + := \ (t, s) → s ≡ 0₂ + +#def is-left-anodyne-left-leg-of-Λ-Λ + : is-left-anodyne ( 2 × 2) + ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) + := + \ A' A α is-left-fib-α → + is-right-orthogonal-to-shape-pushout A' A α + ( 2 × 2) ( \ ts → right-leg-of-Λ ts) (\ ts → left-leg-of-Λ ts) + ( is-left-anodyne-1-right-leg-of-Λ A' A α is-left-fib-α) +``` + +Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the product of +`Δ¹` with the left anodyne pair `{0} ⊂ Δ¹`, hence left anodyne itself. + +```rzk +#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹ uses (extext) + : is-left-anodyne ( 2 × 2) + ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) + := + \ A' A α → + is-right-orthogonal-to-shape-product extext A' A α + 2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) +``` + +Next, we use the left cancellation of left anodyne shape inclusions to deduce +that `Λ ⊂ Δ¹×Δ¹` is left anodyne. + +```rzk +#def is-left-anodyne-Λ-Δ¹×Δ¹ uses (extext) + : is-left-anodyne ( 2 × 2) + ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) + := + is-anodyne-left-cancel-for-shape 2 Δ¹ (\ t → t ≡ 0₂) + ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) + ( is-left-anodyne-left-leg-of-Λ-Λ) + ( is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹) +``` + +Finally, we right cancel the functorial retract `Δ² ⊂ Δ¹×Δ¹` to obtain the +desired left anodyne shape inclusion `Λ ⊂ Δ²`. + +```rzk +#def is-left-anodyne-Λ-Δ² uses (extext) + : is-left-anodyne (2 × 2) + Δ² (\ t → Λ t) + := + is-anodyne-right-cancel-retract-for-shape 2 Δ¹ (\ t → t ≡ 0₂) + ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts) + ( is-functorial-retract-Δ²-Δ¹×Δ¹) + ( is-left-anodyne-Λ-Δ¹×Δ¹) +``` + +which we can unpack to get the desired implication + +```rzk +#def is-inner-fibration-is-left-fibration uses (extext) + ( A' A : U) + ( α : A' → A) + : is-left-fibration A' A α → is-inner-fibration A' A α + := is-left-anodyne-Λ-Δ² A' A α +``` + +### Left fibrations and Segal types + +Since the Segal types are precisely the local types with respect to `Λ ⊂ Δ²`, we +immediately deduce that in any left fibration `α : A' → A`, if `A` is a Segal +type, then so is `A'`. + +```rzk title="RS 17, Theorem 8.8, categorical version" +#def is-segal-domain-left-fibration-is-segal-codomain uses (extext) + ( A' A : U) + ( α : A' → A) + ( is-left-fib-α : is-left-fibration A' A α) + ( is-segal-A : is-segal A) + : is-segal A' + := + is-segal-is-local-horn-inclusion A' + ( is-local-type-right-orthogonal-is-local-type + ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α + ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α) + ( is-local-horn-inclusion-is-segal A is-segal-A)) +``` + +### Discrete types are Segal types + +Another immediate corollary is that every discrete type is Segal. + +```rzk +#def is-segal-is-discrete uses (extext) + ( A : U) + : is-discrete A → is-segal A + := + \ is-discrete-A → + ( is-segal-has-unique-inner-extensions A + ( is-weak-anodyne-is-anodyne-for-shape extext + ( 2) (Δ¹) (\ t → t ≡ 0₂) ( 2 × 2) (Δ²) (\ t → Λ t) + ( is-left-anodyne-Λ-Δ²) + ( A) + ( has-unique-extensions-is-local-type 2 Δ¹ (\ t → t ≡ 0₂) A + ( is-left-local-is-Δ¹-local A + ( is-Δ¹-local-is-discrete A is-discrete-A))))) +``` + +## Discrete types are Segal types (original proof of RS17) + +This chapter contains the original proof of RS17 that discrete types are +automatically Segal types. We retain it since some intermediate calculations +might still be of use. ```rzk #section discrete-arr-equivalences @@ -961,7 +1135,7 @@ general case to the one just proven: Finally, we conclude: ```rzk title="RS17, Proposition 7.3" -#def is-segal-is-discrete uses (extext) +#def is-segal-is-discrete' uses (extext) ( A : U) ( is-discrete-A : is-discrete A) : is-segal A diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 89889f5d..bc10f0e2 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -25,8 +25,6 @@ Some of the definitions in this file rely on extension extensionality: ```rzk #assume extext : ExtExt #assume weakfunext : WeakFunExt -#assume naiveextext : NaiveExtExt - ``` ## Dependent hom types @@ -225,26 +223,20 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`. ### Naive left fibrations are left fibrations -A map `α : A' → A` is called a left fibration if it is right orthogonal to the -shape inclusion `{0} ⊂ Δ¹`. +Recall that a map `α : A' → A` is called a left fibration if it is right +orthogonal to the shape inclusion `{0} ⊂ Δ¹`. + +This notion agrees with that of a naive left fibration. ```rzk -#section is-left-fibration +#section is-left-fibration-is-naive-left-fibration #variables A' A : U #variable α : A' → A -#def is-left-fibration - : U - := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α -``` - -This notion agrees with that of a naive left fibration. - -```rzk #def is-left-fibration-is-naive-left-fibration ( is-nlf : is-naive-left-fibration A A' α) - : is-left-fibration + : is-left-fibration A' A α := \ a' → is-equiv-equiv-is-equiv @@ -259,7 +251,7 @@ This notion agrees with that of a naive left fibration. ( is-nlf (a' 0₂)) #def is-naive-left-fibration-is-left-fibration - ( is-lf : is-left-fibration) + ( is-lf : is-left-fibration A' A α) : is-naive-left-fibration A A' α := \ a' → @@ -277,147 +269,12 @@ This notion agrees with that of a naive left fibration. #def is-naive-left-fibration-iff-is-left-fibration : iff ( is-naive-left-fibration A A' α) - ( is-left-fibration) + ( is-left-fibration A' A α) := ( is-left-fibration-is-naive-left-fibration, is-naive-left-fibration-is-left-fibration) -#end is-left-fibration -``` - -### Left fibrations are inner fibrations - -Recall that an inner fibration is a map `α : A' → A` which is right orthogonal -to `Λ ⊂ Δ²`. - -We aim to show that every left fibration is an inner fibration. This is a -sequence of manipulations where we start with the assumption that `{0} ⊂ Δ¹` is -left orthogonal to `α : A' → A`, i.e. - -```rzk -#section is-inner-fibration-is-left-fibration - -#variables A' A : U -#variable α : A' → A - -#variable is-left-fib-α : is-left-fibration A' A α -``` - -and deduce that various other shape inclusions are left orthogonal as well. - -The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes -`{1} ⊂ right-leg-of-Λ` of `Λ`. - -```rzk - -#def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start - ( B : U) - ( b : B) - : is-equiv - ( ( s : Δ¹) → B [ s ≡ 0₂ ↦ b]) - ( ( (t,s) : right-leg-of-Λ) → B [ s ≡ 0₂ ↦ b]) - ( \ τ (t,s) → τ s) - := - ( ( \ υ s → υ (1₂, s) , \ _ → refl), - ( \ υ s → υ (1₂, s) , \ _ → refl)) - -#def is-right-orthogonal-to-10-1×Δ¹-is-left-fibration uses (is-left-fib-α) - : is-right-orthogonal-to-shape - ( 2 × 2) (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂) A' A α - := - \ ( σ' : ( (t,s) : 2 × 2 | right-leg-of-Λ (t,s) ∧ s ≡ 0₂) → A') → - is-equiv-Equiv-is-equiv' - ( ( s : Δ¹) → A' [s ≡ 0₂ ↦ σ' (1₂, s)]) - ( ( s : Δ¹) → A [s ≡ 0₂ ↦ α (σ' (1₂, s))]) - ( \ τ s → α (τ s)) - ( ( (_, s) : right-leg-of-Λ) → A' [ s ≡ 0₂ ↦ σ' (1₂,s)]) - ( ( (_, s) : right-leg-of-Λ) → A [ s ≡ 0₂ ↦ α ( σ' (1₂,s))]) - ( \ υ ts → α (υ ts)) - ( ( ( \ τ' (t,s) → τ' s , \ τ (t,s) → τ s) , \ _ → refl), - ( is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A' ( σ' (1₂, 0₂)) - , is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A ( α ( σ' (1₂, 0₂))) - ) - ) - ( is-left-fib-α ( \ ( s : 2 | Δ¹ s ∧ s ≡ 0₂) → σ' (1₂,s))) -``` - -Next we use that `Λ` is the pushout of its left leg and its right leg to deduce -that the pair `left-leg-of-Λ ⊂ Λ` is left orthogonal. - -```rzk -#def left-leg-of-Λ : Λ → TOPE - := \ (t, s) → s ≡ 0₂ - -#def is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration uses (is-left-fib-α) - : is-right-orthogonal-to-shape - ( 2 × 2) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) A' A α - := - is-right-orthogonal-to-shape-pushout A' A α - ( 2 × 2) ( \ ts → right-leg-of-Λ ts) (\ ts → left-leg-of-Λ ts) - ( is-right-orthogonal-to-10-1×Δ¹-is-left-fibration) - -``` - -Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the product of -`Δ¹` with the left orthogonal pair `{0} ⊂ Δ¹`, hence left orthogonal itself. - -```rzk -#def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration - uses (naiveextext is-left-fib-α) - : is-right-orthogonal-to-shape - ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) A' A α - := - is-right-orthogonal-to-shape-product naiveextext A' A α - 2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α -``` - -Next, we use the left cancellation of left orthogonal shape inclusions to deduce -that `Λ ⊂ Δ¹×Δ¹` is left orthogonal to `α : A' → A`. - -```rzk -#def is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration - uses (naiveextext is-left-fib-α) - : is-right-orthogonal-to-shape - ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) A' A α - := - is-right-orthogonal-to-shape-left-cancel A' A α - ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) - ( is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration) - ( is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration) -``` - -Finally, we right cancel the functorial retract `Δ² ⊂ Δ¹×Δ¹` to obtain the -desired left orthogonal shape inclusion `Λ ⊂ Δ²`. - -```rzk -#def is-inner-fibration-is-left-fibration uses (naiveextext is-left-fib-α) - : is-inner-fibration A' A α - := - is-right-orthogonal-to-shape-right-cancel-retract A' A α - ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts) - ( is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration) - ( Δ²-is-functorial-retract-Δ¹×Δ¹) - -#end is-inner-fibration-is-left-fibration -``` - -Since the Segal types are precisely the local types with respect to `Λ ⊂ Δ¹`, we -immediately deduce that in any left fibration `α : A' → A`, if `A` is a Segal -type, then so is `A'`. - -```rzk title="Theorem 8.8, categorical version" -#def is-segal-domain-left-fibration-is-segal-codomain uses (naiveextext) - ( A' A : U) - ( α : A' → A) - ( is-left-fib-α : is-left-fibration A' A α) - ( is-segal-A : is-segal A) - : is-segal A' - := - is-segal-is-local-horn-inclusion A' - ( is-local-type-right-orthogonal-is-local-type - ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α - ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α) - ( is-local-horn-inclusion-is-segal A is-segal-A)) +#end is-left-fibration-is-naive-left-fibration ``` ### Naive left fibrations vs. covariant families @@ -597,13 +454,13 @@ fibration, hence an inner fibration. It immediately follows that if `A` is Segal, then so is `Σ A, C`. ```rzk title="RS17, Theorem 8.8" -#def is-segal-total-type-covariant-family-is-segal-base uses (naiveextext) +#def is-segal-total-type-covariant-family-is-segal-base uses (extext) ( A : U) ( C : A → U) ( is-covariant-C : is-covariant A C) : is-segal A → is-segal (total-type A C) := - is-segal-domain-left-fibration-is-segal-codomain + is-segal-domain-left-fibration-is-segal-codomain extext ( total-type A C) A (\ (a,_) → a) ( is-left-fibration-is-naive-left-fibration ( total-type A C) A (\ (a,_) → a) diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md index 0af7298a..c38eb081 100644 --- a/src/simplicial-hott/13-limits.rzk.md +++ b/src/simplicial-hott/13-limits.rzk.md @@ -8,11 +8,12 @@ This is a literate `rzk` file: #lang rzk-1 ``` -Some definitions make use of function extentionality. +Some definitions make use of function extentionality and extension +extensionality. ```rzk #assume funext : FunExt -#assume naiveextext : NaiveExtExt +#assume extext : ExtExt ``` ## Definition limits and colimits @@ -262,14 +263,14 @@ The type of cocones of a function with codomain a Segal type is a Segal type. ( f)) ( \ b → constant A B b) -#def is-segal-cocone-is-segal uses (funext) +#def is-segal-cocone-is-segal uses (funext extext) ( A B : U) ( is-segal-B : is-segal B) ( f : A → B) : is-segal ( cocone A B f) := is-segal-total-type-covariant-family-is-segal-base - ( naiveextext) + ( extext) ( B) ( family-cocone A B f) ( is-covariant-family-cone-is-segal @@ -283,7 +284,7 @@ The type of cocones of a function with codomain a Segal type is a Segal type. Colimits are unique up to isomorphism. ```rzk title="BM, Corollary 1 (i)" -#def iso-colimit-is-segal uses ( naiveextext funext) +#def iso-colimit-is-segal uses ( extext funext) ( A B : U) ( is-segal-B : is-segal B) ( f : A → B)