From 3098910b634e195879af8d04c39d274df97c552c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 21:17:49 +0200
Subject: [PATCH 1/2] fibers between segal types

---
 src/simplicial-hott/05-segal-types.rzk.md | 48 ++++++++++++++++++++++-
 1 file changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index ed74e32c..b8019dc9 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/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
+  ( 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))
+```

From b84295ef3cce02adf13e837ecf908e355ff40113 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 21:20:26 +0200
Subject: [PATCH 2/2] make usage of extext explicit

---
 src/simplicial-hott/05-segal-types.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index b8019dc9..0ad043a6 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1896,7 +1896,7 @@ 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
+#def is-fiberwise-segal-are-segal uses (extext weakextext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)