Merge branch 'main' into issue-24

rzk.yaml

@@ -0,0 +1,3 @@
+include:
+  - src/hott/**/*.rzk.md
+  - src/simplicial-hott/**/*.rzk.md

src/hott/03-equivalences.rzk.md

@@ -314,6 +314,43 @@ Now we compose the functions that are equivalences.
   := equiv-comp B A C (inv-equiv A B A≃B) (A≃C)
 ```
 
+```rzk title="Right cancellation of equivalence property in diagrammatic order"
+#def ap-cancel-has-retraction
+  ( B C : U)
+  ( g : B → C)
+  ( (retr-g, η-g) : has-retraction B C g)
+  ( b b' : B)
+  : (g b = g b') → (b = b')
+  :=
+    \ gp →
+      triple-concat B b (retr-g (g b)) (retr-g (g b')) b'
+        (rev B (retr-g (g b)) b
+          (η-g b))
+        (ap C B (g b) (g b') retr-g gp)
+        (η-g b')
+
+
+#def is-equiv-right-cancel
+  ( A B C : U)
+  ( f : A → B)
+  ( g : B → C)
+  ( (has-retraction-g, (sec-g, ε-g)) : is-equiv B C g)
+  ( ((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 → -- need (f ∘ sec-gf ∘ g) b = b
+      ap-cancel-has-retraction B C g has-retraction-g (f (sec-gf (g b))) b
+      (ε-gf (g b)) -- have g (f ∘ sec-gf ∘ g) b) = g b
+    )
+    )
+
+```
+
 ```rzk title="A composition of three equivalences"
 #def equiv-triple-comp
   ( A B C D : U)

src/hott/08-families-of-maps.rzk.md

@@ -812,3 +812,76 @@ types over a product type.
 
 #end fibered-map-over-product
 ```
+
+## Homotopy cartesian squares
+
+
+```rzk
+#def is-homotopy-cartesian
+  ( A' : U)
+  ( C' : A' → U)
+  ( A : U)
+  ( C : A → U)
+  ( f : A' → A)
+  ( F : (a' : A') → C' a' → C (f a'))
+  : U
+  :=
+    (a' : A') → is-equiv (C' a') (C (f a')) (F a')
+
+#def homotopy-cartesian-square
+  ( A' : U)
+  ( C' : A' → U)
+  ( A : U)
+  ( C : A → U)
+  : U
+  := Σ (f : A' → A), Σ (F : (a' : A') → C' a' → C (f a')),
+    is-homotopy-cartesian A' C' A C f F
+
+
+#section homotopy-cartesian-pasting
+
+#variable A'' : U
+#variable C'' : A'' → U
+#variable A' : U
+#variable C' : A' → U
+#variable A : U
+#variable C : A → U
+#variable f' : A'' → A'
+#variable F' : (a'' : A'') → C'' a'' → C' (f' a'')
+#variable f : A' → A
+#variable F : (a' : A') → C' a' → C (f a')
+
+#def is-homotopy-cartesian-composition
+  : is-homotopy-cartesian A'' C'' A' C' f' F' →
+    is-homotopy-cartesian A' C' A C f F →
+    is-homotopy-cartesian A'' C'' A C
+      (comp A'' A' A
+        f f')
+      (\ a'' →
+        comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+          (F (f' a'')) (F' a'')
+      )
+  :=
+    \ ihc' ihc a'' →
+    is-equiv-comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      (F' a'') (ihc' a'')
+      (F (f' a'')) (ihc (f' a''))
+
+#def is-homotopy-cartesian-cancellation
+  : is-homotopy-cartesian A' C' A C f F
+  → is-homotopy-cartesian A'' C'' A C
+      (comp A'' A' A f f')
+      (\ a'' →
+        comp (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+          (F (f' a'')) (F' a'')
+      )
+  → is-homotopy-cartesian A'' C'' A' C' f' F'
+  :=
+    \ ihc ihc'' a'' →
+    is-equiv-right-cancel (C'' a'') (C' (f' a'')) (C (f (f' a'')))
+      (F' a'') (F (f' a''))
+      (ihc (f' a''))
+      (ihc'' a'')
+
+#end homotopy-cartesian-pasting
+```

src/simplicial-hott/04-extension-types.rzk.md

@@ -288,14 +288,28 @@ cases an extension type to a function type.
 #define is-contr-ext-based-paths uses (weak-ext-ext f)
   : is-contr ((t : ψ ) → (Σ (y : A t) ,
               ((ext-projection-temp) t = y))[ϕ t ↦ (a t , refl)])
-  := weak-ext-ext
-      ( I )
-      ( ψ )
-      ( ϕ )
-      ( \ t → (Σ (y : A t) , ((ext-projection-temp) t = y)))
-      ( \ t →
-            is-contr-based-paths (A t ) ((ext-projection-temp) t))
-      ( \ t → (a t , refl) )
+  :=
+    weak-ext-ext
+    ( I )
+    ( ψ )
+    ( ϕ )
+    ( \ t → (Σ (y : A t) , ((ext-projection-temp) t = y)))
+    ( \ t →
+      is-contr-based-paths (A t ) ((ext-projection-temp) t))
+    ( \ t → (a t , refl) )
+
+#define is-contr-ext-codomain-based-paths uses (weak-ext-ext f)
+  : is-contr
+    ( ( t : ψ) →
+      ( Σ (y : A t) , (y = ext-projection-temp t)) [ ϕ t ↦ (a t , refl)])
+  :=
+    weak-ext-ext
+    ( I)
+    ( ψ)
+    ( ϕ)
+    ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
+    ( \ t → is-contr-codomain-based-paths (A t) (ext-projection-temp t))
+    ( \ t → (a t , refl))
 
 #define is-contr-based-paths-ext uses (weak-ext-ext)
   : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
@@ -334,10 +348,10 @@ The map that defines extension extensionality
         ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
   :=
     total-map
-      ( (t : ψ ) → A t [ϕ t ↦ a t])
-      ( \ g → (f = g))
-      ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
-      ( ext-htpy-eq I ψ ϕ A a f)
+    ( (t : ψ ) → A t [ϕ t ↦ a t])
+    ( \ g → (f = g))
+    ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
+    ( ext-htpy-eq I ψ ϕ A a f)
 ```
 
 The total bundle version of extension extensionality
@@ -357,14 +371,14 @@ The total bundle version of extension extensionality
                (ext-ext-weak-ext-ext-map I ψ ϕ A a f)
   :=
     is-equiv-are-contr
-      ((Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g))  )
-      ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
+    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)  )
+    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
       ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
-      ( is-contr-based-paths
-        ( (t : ψ ) → A t [ϕ t ↦ a t])
-        ( f ))
-      ( is-contr-based-paths-ext weak-ext-ext I ψ ϕ A a f)
-      ( ext-ext-weak-ext-ext-map I ψ ϕ A a f)
+    ( is-contr-based-paths
+      ( (t : ψ ) → A t [ϕ t ↦ a t])
+      ( f ))
+    ( is-contr-based-paths-ext weak-ext-ext I ψ ϕ A a f)
+    ( ext-ext-weak-ext-ext-map I ψ ϕ A a f)
 ```
 
 Finally, using equivalences between families of equivalences and bundles of
@@ -399,7 +413,7 @@ extension extensionality that we get by extraccting the fiberwise equivalence.
 ```rzk title="RS17 Proposition 4.8(i)"
 #define ext-ext-weak-ext-ext
   (weak-ext-ext : WeakExtExt)
-   :  ExtExt
+  :  ExtExt
   := \ I ψ ϕ A a f g →
       ext-ext-weak-ext-ext' weak-ext-ext I ψ ϕ A a f g
 ```
@@ -465,3 +479,59 @@ equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
               ( b)
               ( \ t → second (second (second (famequiv t))) (b t))))))
 ```
+
+We have a homotopy extension property.
+
+The following code is another instantiation of casting, necessary for some
+arguments below.
+
+```rzk
+#define restrict
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → A t [ϕ t ↦ a t])
+  : (t : ψ ) → A t
+  := f
+
+```
+
+The homotopy extension property follows from a straightforward application of
+the axiom of choice to the point of contraction for weak extension
+extensionality.
+
+```rzk title="RS17 Proposition 4.10"
+#define htpy-ext-property
+  ( weak-ext-ext : WeakExtExt)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : ψ → U)
+  ( b : (t : ψ) → A t)
+  ( a : (t : ϕ) → A t)
+  ( e : (t : ϕ) → a t = b t)
+  : Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) ,
+      ((t : ψ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
+  :=
+    first
+    ( axiom-choice
+      ( I)
+      ( ψ)
+      ( ϕ)
+      ( A)
+      ( \ t y → y = b t)
+      ( a)
+      ( e))
+    ( first
+      ( weak-ext-ext
+        ( I)
+        ( ψ)
+        ( ϕ)
+        ( \ t → (Σ (y : A t) , y = b t))
+        ( \ t → is-contr-codomain-based-paths
+                ( A t)
+                ( b t))
+        ( \ t → ( a t , e t) )))
+```

src/simplicial-hott/05-segal-types.rzk.md

@@ -72,6 +72,27 @@ are called the coslice and slice, respectively.
   := Σ (z : A) , (hom A z a)
 ```
 
+The types `coslice A a` and `slice A a`
+are functorial in `A` in the following sense:
+
+```rzk
+#def coslice-fun
+  (A B : U)
+  (f : A → B)
+  (a : A)
+  : coslice A a → coslice B (f a)
+  :=
+    \ (a', g) → (f a', \ t → f (g t))
+
+#def slice-fun
+  (A B : U)
+  (f : A → B)
+  (a : A)
+  : slice A a → slice B (f a)
+  :=
+    \ (a', g) → (f a', \ t → f (g t))
+```
+
 Extension types are also used to define the type of commutative triangles:
 
 <svg style="float: right" viewBox="0 0 200 200" width="150" height="200">

src/simplicial-hott/06-2cat-of-segal-types.rzk.md

@@ -318,3 +318,61 @@ the "Gray interchanger" built from two commutative triangles.
     ( horizontal-comp-nat-trans A B C f g f' g' η η')
   := \ (t, s) a → η' t (η s a)
 ```
+
+### Naturality square
+
+```rzk title="RS17, Proposition 6.6"
+#section comp-eq-square-is-segal
+
+#variable A : U
+#variable is-segal-A : is-segal A
+#variable α : (Δ¹×Δ¹) → A
+
+#def α00 : A := α (0₂,0₂)
+#def α01 : A := α (0₂,1₂)
+#def α10 : A := α (1₂,0₂)
+#def α11 : A := α (1₂,1₂)
+
+#def α0* : Δ¹ → A := \ t → α (0₂,t)
+#def α1* : Δ¹ → A := \ t → α (1₂,t)
+#def α*0 : Δ¹ → A := \ s → α (s,0₂)
+#def α*1 : Δ¹ → A := \ s → α (s,1₂)
+#def α-diag : Δ¹ → A := \ s → α (s,s)
+
+#def lhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α01 α11 α0* α*1
+#def rhs uses (α) : Δ¹ → A := comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
+
+#def lower-triangle-square : hom2 A α00 α01 α11 α0* α*1 α-diag
+  := \ (s, t) → α (t,s)
+
+#def upper-triangle-square : hom2 A α00 α10 α11 α*0 α1* α-diag
+  := \ (s,t) → α (s,t)
+
+#def comp-eq-square-is-segal uses (α)
+  : comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 =
+    comp-is-segal A is-segal-A α00 α10 α11 α*0 α1*
+  :=
+    zig-zag-concat (hom A α00 α11) lhs α-diag rhs
+    ( uniqueness-comp-is-segal A is-segal-A α00 α01 α11 α0* α*1 α-diag
+      ( lower-triangle-square))
+    ( uniqueness-comp-is-segal A is-segal-A α00 α10 α11 α*0 α1* α-diag
+      ( upper-triangle-square))
+
+
+#end comp-eq-square-is-segal
+
+#def naturality-nat-trans-is-segal
+  (A B : U)
+  (is-segal-B : is-segal B)
+  (f g : A → B)
+  (α : hom (A → B) f g)
+  (x y : A)
+  (k : hom A x y)
+  : comp-is-segal B is-segal-B (f x) (f y) (g y)
+    ( ap-hom A B f x y k)
+    ( \ s → α s y) =
+    comp-is-segal B is-segal-B (f x) (g x) (g y)
+    ( \ s → α s x)
+    ( ap-hom A B g x y k)
+  := comp-eq-square-is-segal B is-segal-B (\ (s,t) → α s (k t))
+```