Merge pull request #122 from TashiWalde/fibers-between-segal

Fibers between Segal types are Segal

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

@@ -417,7 +417,7 @@ for the inclusion `Λ ⊂ Δ¹`.
   : U → U
   := is-local-type (2 × 2) Δ² (\ t → Λ t)
 
-#def is-local-horn-inclusion-unpacked
+#def unpack-is-local-horn-inclusion
   ( A : U)
   : is-local-horn-inclusion A = is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
   := refl
@@ -570,6 +570,28 @@ We have now proven that both notions of Segal types are logically equivalent.
   := (is-local-horn-inclusion-is-segal A , is-segal-is-local-horn-inclusion A)
 ```
 
+Similarly, Segal types are characterized by having unique extensions along
+`Λ ⊂ Δ²`.
+
+```rzk
+#def is-segal-has-unique-inner-extensions
+  ( A : U)
+  ( has-inner-ue-A : has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A)
+  : is-segal A
+  :=
+    is-segal-is-local-horn-inclusion A
+    ( is-local-type-has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A
+      has-inner-ue-A)
+
+#def has-unique-inner-extensions-is-segal
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  : has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A
+  :=
+    has-unique-extensions-is-local-type (2 × 2) (Δ²) (\ t → Λ t) A
+    ( is-local-horn-inclusion-is-segal A is-segal-A)
+```
+
 ## Segal function and extension types
 
 Using the new characterization of Segal types, we can show that the type of
@@ -1866,3 +1888,27 @@ products of morphisms. It is implicitly stated in Proposition 8.21.
 
 #end morphisms-of-products-is-products-of-morphisms
 ```
+
+## Fibers of maps between Segal types
+
+For any map `f : A → B` between Segal types, each fiber `fib A B f b` is again a
+Segal type. This is an instance of a general statement about types with unique
+extensions for the shape inclusion `Λ ⊂ Δ²`.
+
+```rzk
+#def is-fiberwise-segal-are-segal uses (extext weakextext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-segal-A : is-segal A)
+  ( is-segal-B : is-segal B)
+  ( b : B)
+  : is-segal (fib A B f b)
+  :=
+    is-segal-has-unique-inner-extensions (fib A B f b)
+    ( has-fiberwise-unique-extensions-have-unique-extensions
+      extext weakextext
+      ( 2 × 2) (Δ²) (\ t → Λ t) A B f
+      ( has-unique-inner-extensions-is-segal A is-segal-A)
+      ( has-unique-inner-extensions-is-segal B is-segal-B)
+      ( b))
+```