From c4b929d50a8c59d146e04f0ad607885f80e1849c Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Sun, 21 Jul 2024 12:18:28 +0200
Subject: [PATCH 1/9] experiments with 2-Segal types

---
 src/2Segal/2segal-types.rzk.md | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 src/2Segal/2segal-types.rzk.md

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
new file mode 100644
index 00000000..10a2e77c
--- /dev/null
+++ b/src/2Segal/2segal-types.rzk.md
@@ -0,0 +1,31 @@
+# 2-Segal spaces
+
+Experimental formalization project on 2-Segal spaces.
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+```rzk
+#def is-2segal-local
+  ( A : U)
+  : U
+  :=
+    product
+      ( is-local-type (2 × 2 × 2) Δ³ Λ³₁ A)
+      ( is-local-type (2 × 2 × 2) Δ³ Λ³₂ A)
+```
+
+```rzk
+-- #def 3hornfill1
+--   ( A : U)
+--   : U
+--   :=
+--     ( x : A) → (y : A) → (z : A) → (w : A)
+--   → ( f : hom A x y) → (g : hom A y z) → (h : hom A x z)
+--   → ( b : hom A x w) → (d : hom A y w) → (e : hom A z w)
+--   → ( α : hom2 A x y z f g h) → (β : hom2 A x y w f d b)
+--   → ( γ : hom2 A x z w h d e)
+```

From a4b7b7a374979ae2674b4ec37724241474e2bd22 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Sun, 21 Jul 2024 19:17:49 +0200
Subject: [PATCH 2/9] 2segal

---
 src/2Segal/2segal-types.rzk.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index 10a2e77c..cc0746af 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -9,13 +9,13 @@ This is a literate `rzk` file:
 ```
 
 ```rzk
-#def is-2segal-local
-  ( A : U)
-  : U
-  :=
-    product
-      ( is-local-type (2 × 2 × 2) Δ³ Λ³₁ A)
-      ( is-local-type (2 × 2 × 2) Δ³ Λ³₂ A)
+-- #def is-2segal-local
+--   ( A : U)
+--   : U
+--   :=
+--     product
+--      ( is-local-type (2 × 2 × 2) Δ³ (2segalhorn1) A)
+--      ( is-local-type (2 × 2 × 2) Δ³ (2segalhorn2) A)
 ```
 
 ```rzk

From 9ef7e9446a8796d014cb7f8139fc66ab38af6eb8 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Mon, 22 Jul 2024 00:02:53 +0200
Subject: [PATCH 3/9] 2segal

---
 src/2Segal/2segal-types.rzk.md | 32 +++++++++++++++++++++++++-------
 1 file changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index cc0746af..aeaedd2d 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -8,14 +8,32 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
+### The 3 dimensional 2-Segal horns
+
 ```rzk
--- #def is-2segal-local
---   ( A : U)
---   : U
---   :=
---     product
---      ( is-local-type (2 × 2 × 2) Δ³ (2segalhorn1) A)
---      ( is-local-type (2 × 2 × 2) Δ³ (2segalhorn2) A)
+#def Δ³₍₀₂₎
+  : Δ³ → TOPE
+  :=
+    \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t3 ≡ t2
+
+#def Δ³₍₁₃₎
+  : Δ³ → TOPE
+  :=
+    \ ((t1 , t2) , t3) → t2 ≡ t1 ∨ t1 ≡ 1₂
+```
+
+### 2-Segal types
+
+A type is 2-Segal if it is local with respect to 2-Segal horn inclusions.
+
+```rzk
+#def is-2segal-local
+  ( A : U)
+  : U
+  :=
+    product
+     ( is-local-type (2 × 2 × 2) Δ³ Δ³₍₀₂₎ A)
+     ( is-local-type (2 × 2 × 2) Δ³ Δ³₍₁₃₎ A)
 ```
 
 ```rzk

From 6d0b5496b23aaf20dd4e9b5e9ea9f6499717b6e1 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Tue, 23 Jul 2024 16:39:04 +0200
Subject: [PATCH 4/9] 2segal

---
 src/2Segal/2segal-types.rzk.md | 128 ++++++++++++++++++++++++++++-----
 1 file changed, 109 insertions(+), 19 deletions(-)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index aeaedd2d..c7f7cc76 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -10,40 +10,130 @@ This is a literate `rzk` file:
 
 ### The 3 dimensional 2-Segal horns
 
-```rzk
-#def Δ³₍₀₂₎
+```rzkx
+#def Λ³₍₀₂₎
   : Δ³ → TOPE
   :=
-    \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t3 ≡ t2
+    \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t1 ≡ t2 -- This could be t3==t2.
 
-#def Δ³₍₁₃₎
+#def Λ³₍₁₃₎
   : Δ³ → TOPE
   :=
-    \ ((t1 , t2) , t3) → t2 ≡ t1 ∨ t1 ≡ 1₂
+    \ ((t1 , t2) , t3) → t2 ≡ t3 ∨ t1 ≡ 1₂ -- This could be t1==t2.
 ```
 
 ### 2-Segal types
 
-A type is 2-Segal if it is local with respect to 2-Segal horn inclusions.
+We use the conventions from the definition of `#!rzk hom3` from
+`11-adjunctions.rzk`.
 
 ```rzk
-#def is-2segal-local
+#def is-2-segal₍₀₂₎
   ( A : U)
   : U
   :=
-    product
-     ( is-local-type (2 × 2 × 2) Δ³ Δ³₍₀₂₎ A)
-     ( is-local-type (2 × 2 × 2) Δ³ Δ³₍₁₃₎ A)
+    ( w : A) → (x : A) → (y : A) → (z : A)
+  → ( f : hom A w x) → (gf : hom A w y) → (hgf : hom A w z)
+  → ( g : hom A x y) → (h : hom A y z)
+  → ( α₃ : hom2 A w x y f g gf) → (α₁ : hom2 A w y z gf h hgf)
+  → is-contr
+      ( Σ ( hg : hom A x z)
+      , ( Σ ( α₂ : hom2 A w x z f hg hgf)
+        , ( Σ ( α₀ : hom2 A x y z g h hg)
+            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
+
+#def is-2-segal₍₁₃₎
+  ( A : U)
+  : U
+  :=
+    ( w : A) → (x : A) → (y : A) → (z : A)
+  → ( f : hom A w x) → (hgf : hom A w z)
+  → ( g : hom A x y) → (hg : hom A x z) → (h : hom A y z)
+  → ( α₂ : hom2 A w x z f hg hgf) → (α₀ : hom2 A x y z g h hg)
+  → is-contr
+      ( Σ ( gf : hom A w y)
+      , ( Σ ( α₃ : hom2 A w x y f g gf)
+        , ( Σ ( α₁ : hom2 A w y z gf h hgf)
+            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
+
+#def is-2-segal
+  ( A : U)
+  : U
+  :=
+    product (is-2-segal₍₀₂₎ A) (is-2-segal₍₁₃₎ A)
+```
+
+```rzk
+#def 3horn₍₀₂₎
+  ( A : U)
+  ( w x y z : A)
+  ( f : hom A w x)
+  ( gf : hom A w y)
+  ( hgf : hom A w z)
+  ( g : hom A x y)
+  ( h : hom A y z)
+  ( α₃ : hom2 A w x y f g gf)
+  ( α₁ : hom2 A w y z gf h hgf)
+  : Λ³₍₀₂₎ → A
+  :=
+    \ ((t₁ , t₂) , t₃) →
+      recOR
+        ( t₃ ≡ 0₂ ↦ α₃ (t₁ , t₂)
+        , t₁ ≡ t₂ ↦ α₁ (t₁ , t₃)) -- This could be t3==t2.
+
+#def 3horn₍₁₃₎
+  ( A : U)
+  ( w x y z : A)
+  ( f : hom A w x)
+  ( hgf : hom A w z)
+  ( g : hom A x y)
+  ( hg : hom A x z)
+  ( h : hom A y z)
+  ( α₂ : hom2 A w x z f hg hgf)
+  ( α₀ : hom2 A x y z g h hg)
+  : Λ³₍₁₃₎ → A
+  :=
+  \ ((t₁ , t₂) , t₃) →
+    recOR
+      ( t₂ ≡ t₃ ↦ α₂ (t₁ , t₃) -- This could be t1==t2.
+      , t₁ ≡ 1₂ ↦ α₀ (t₂ , t₃))
+
+#def associators-are-3horn-fillings₍₀₂₎
+  ( A : U)
+  ( w x y z : A)
+  ( f : hom A w x)
+  ( gf : hom A w y)
+  ( hgf : hom A w z)
+  ( g : hom A x y)
+  ( h : hom A y z)
+  ( α₃ : hom2 A w x y f g gf)
+  ( α₁ : hom2 A w y z gf h hgf)
+  : Equiv
+      ( Σ ( hg : hom A x z)
+      , ( Σ ( α₂ : hom2 A w x z f hg hgf)
+        , ( Σ ( α₀ : hom2 A x y z g h hg)
+            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
+      ( ( t : Δ³) → A [Λ³₍₀₂₎ t ↦ 3horn₍₀₂₎ A w x y z f gf hgf g h α₃ α₁ t])
+  :=
+    ( \ H t → second (second (second H)) t
+      , ( ( \ k → (\ t → k ((t , t) , t)
+          , ( \ (t , s) → k ((t , s) , s)
+            , ( \ (t , s) → k ((1₂ , t) , s)
+              , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
+        , \ H → refl)
+          , ( U , U)
+      )
+    )
 ```
 
+A type is 2-Segal if it is local with respect to 2-Segal horn inclusions.
+
 ```rzk
--- #def 3hornfill1
---   ( A : U)
---   : U
---   :=
---     ( x : A) → (y : A) → (z : A) → (w : A)
---   → ( f : hom A x y) → (g : hom A y z) → (h : hom A x z)
---   → ( b : hom A x w) → (d : hom A y w) → (e : hom A z w)
---   → ( α : hom2 A x y z f g h) → (β : hom2 A x y w f d b)
---   → ( γ : hom2 A x z w h d e)
+#def is-local-2-segal-horn-inclusion
+  ( A : U)
+  : U
+  :=
+    product
+     ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₀₂₎ A)
+     ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₁₃₎ A)
 ```

From a10d4b01a9cc9ac57209344265bc9226c1caffc1 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Tue, 23 Jul 2024 18:46:25 +0200
Subject: [PATCH 5/9] 3-horn combinatorics

---
 rzk.yaml                       |  1 +
 src/2Segal/2segal-types.rzk.md | 45 ++++++++++++++++++++++++++++------
 2 files changed, 39 insertions(+), 7 deletions(-)

diff --git a/rzk.yaml b/rzk.yaml
index 4c2fc69f..b7e9efdf 100644
--- a/rzk.yaml
+++ b/rzk.yaml
@@ -1,3 +1,4 @@
 include:
   - src/hott/**/*.rzk.md
   - src/simplicial-hott/**/*.rzk.md
+  - src/2Segal/**/*.rzk.md
diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index c7f7cc76..a50b6d74 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -10,7 +10,7 @@ This is a literate `rzk` file:
 
 ### The 3 dimensional 2-Segal horns
 
-```rzkx
+```rzk
 #def Λ³₍₀₂₎
   : Δ³ → TOPE
   :=
@@ -116,17 +116,48 @@ We use the conventions from the definition of `#!rzk hom3` from
       ( ( t : Δ³) → A [Λ³₍₀₂₎ t ↦ 3horn₍₀₂₎ A w x y z f gf hgf g h α₃ α₁ t])
   :=
     ( \ H t → second (second (second H)) t
-      , ( ( \ k → (\ t → k ((t , t) , t)
+      , ( ( ( \ k → (\ t → k ((1₂ , t) , t)
           , ( \ (t , s) → k ((t , s) , s)
             , ( \ (t , s) → k ((1₂ , t) , s)
               , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
-        , \ H → refl)
-          , ( U , U)
-      )
-    )
+          , \ H → refl))
+        , ( ( \ k → (\ t → k ((1₂ , t) , t)
+            , ( \ (t , s) → k ((t , s) , s)
+              , ( \ (t , s) → k ((1₂ , t) , s)
+                , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
+            , \ H → refl))))
+
+#def associators-are-3horn-fillings₍₁₃₎
+  ( A : U)
+  ( w x y z : A)
+  ( f : hom A w x)
+  ( hgf : hom A w z)
+  ( g : hom A x y)
+  ( hg : hom A x z)
+  ( h : hom A y z)
+  ( α₂ : hom2 A w x z f hg hgf)
+  ( α₀ : hom2 A x y z g h hg)
+  : Equiv
+      ( Σ ( gf : hom A w y)
+      , ( Σ ( α₃ : hom2 A w x y f g gf)
+        , ( Σ ( α₁ : hom2 A w y z gf h hgf)
+            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
+      ( ( t : Δ³) → A [Λ³₍₁₃₎ t ↦ 3horn₍₁₃₎ A w x y z f hgf g hg h α₂ α₀ t])
+  :=
+    ( \ H t → second (second (second H)) t
+      , ( ( ( \ k → (\ t → k ((t , t) , 0₂)
+          , ( \ (t , s) → k ((t , s) , 0₂)
+            , ( \ (t , s) → k ((t , t) , s)
+              , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
+          , \ H → refl))
+        , ( ( \ k → (\ t → k ((t , t) , 0₂)
+            , ( \ (t , s) → k ((t , s) , 0₂)
+              , ( \ (t , s) → k ((t , t) , s)
+                , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
+            , \ H → refl))))
 ```
 
-A type is 2-Segal if it is local with respect to 2-Segal horn inclusions.
+A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
 
 ```rzk
 #def is-local-2-segal-horn-inclusion

From 43f3339ef67eb4d06de5237c6f5135b77a05b1b7 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Thu, 25 Jul 2024 13:37:58 +0200
Subject: [PATCH 6/9] 2segal

---
 src/2Segal/2segal-types.rzk.md | 101 +++++++++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index a50b6d74..b13bf00d 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -8,6 +8,12 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
+```rzk
+#assume funext : FunExt
+-- #assume weakextext : WeakExtExt
+-- #assume extext : ExtExt
+```
+
 ### The 3 dimensional 2-Segal horns
 
 ```rzk
@@ -20,6 +26,16 @@ This is a literate `rzk` file:
   : Δ³ → TOPE
   :=
     \ ((t1 , t2) , t3) → t2 ≡ t3 ∨ t1 ≡ 1₂ -- This could be t1==t2.
+
+#def 3-horn-restriction₍₀₂₎
+  ( A : U)
+  : ( Δ³ → A) → (Λ³₍₀₂₎ → A)
+  := \ f t → f t
+
+#def 3-horn-restriction₍₁₃₎
+  ( A : U)
+  : ( Δ³ → A) → (Λ³₍₁₃₎ → A)
+  := \ f t → f t
 ```
 
 ### 2-Segal types
@@ -157,6 +173,21 @@ We use the conventions from the definition of `#!rzk hom3` from
             , \ H → refl))))
 ```
 
+A type is 2-Segal if and only if its based hom-types are Segal.
+
+```rzk
+#def test45
+  ( A : U)
+  ( w x y : A)
+  ( f : hom A w x)
+  ( gf : hom A w y)
+  ( g : hom A x y)
+  ( α₃ : hom2 A w x y f g gf)
+  : hom (coslice A w) (x , f) (y , gf)
+  :=
+    U
+```
+
 A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
 
 ```rzk
@@ -168,3 +199,73 @@ A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
      ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₀₂₎ A)
      ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₁₃₎ A)
 ```
+
+The proof of `is-local-horn-inclusion-function-type` works for 2-segal types by
+just changing the horns.
+
+```rzk
+#def is-local-2-segal-horn-inclusion-function-type uses (funext)
+  ( X : U)
+  ( A : X → U)
+  ( fiberwise-is-2-segal-A : (x : X) → is-local-2-segal-horn-inclusion (A x))
+  : is-local-2-segal-horn-inclusion ((x : X) → A x)
+  :=
+    ( ( is-equiv-triple-comp
+        ( Δ³ → ((x : X) → A x))
+        ( ( x : X) → Δ³ → A x)
+        ( ( x : X) → Λ³₍₀₂₎ → A x)
+        ( Λ³₍₀₂₎ → ((x : X) → A x))
+        ( \ g x t → g t x) -- first equivalence
+        ( second (flip-ext-fun
+          ( 2 × 2 × 2)
+          ( Δ³)
+          ( \ t → BOT)
+          ( X)
+          ( \ t → A)
+          ( \ t → recBOT)))
+        ( \ h x t → h x t) -- second equivalence
+        ( second (equiv-function-equiv-family
+          ( funext)
+          ( X)
+          ( \ x → (Δ³ → A x))
+          ( \ x → (Λ³₍₀₂₎ → A x))
+          ( \ x → (3-horn-restriction₍₀₂₎ (A x)
+            , first (fiberwise-is-2-segal-A x)))))
+        ( \ h t x → (h x) t) -- third equivalence
+        ( second (flip-ext-fun-inv
+          ( 2 × 2 × 2)
+          ( \ t → Λ³₍₀₂₎ t)
+          ( \ t → BOT)
+          ( X)
+          ( \ t → A)
+          ( \ t → recBOT))))
+          , ( is-equiv-triple-comp
+              ( Δ³ → ((x : X) → A x))
+              ( ( x : X) → Δ³ → A x)
+              ( ( x : X) → Λ³₍₁₃₎ → A x)
+              ( Λ³₍₁₃₎ → ((x : X) → A x))
+              ( \ g x t → g t x) -- first equivalence
+              ( second (flip-ext-fun
+                ( 2 × 2 × 2)
+                ( Δ³)
+                ( \ t → BOT)
+                ( X)
+                ( \ t → A)
+                ( \ t → recBOT)))
+              ( \ h x t → h x t) -- second equivalence
+              ( second (equiv-function-equiv-family
+                ( funext)
+                ( X)
+                ( \ x → (Δ³ → A x))
+                ( \ x → (Λ³₍₁₃₎ → A x))
+                ( \ x → (3-horn-restriction₍₁₃₎ (A x)
+                  , second (fiberwise-is-2-segal-A x)))))
+              ( \ h t x → (h x) t) -- third equivalence
+              ( second (flip-ext-fun-inv
+                ( 2 × 2 × 2)
+                ( \ t → Λ³₍₁₃₎ t)
+                ( \ t → BOT)
+                ( X)
+                ( \ t → A)
+                ( \ t → recBOT)))))
+```

From 761153aa3d800407ea9bfb68a3e1fc2f5efd8e67 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Fri, 26 Jul 2024 23:03:12 +0200
Subject: [PATCH 7/9] generalization of proofs for Segal types

---
 src/2Segal/2segal-types.rzk.md | 222 ++++++++++++++++++++++-----------
 1 file changed, 149 insertions(+), 73 deletions(-)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index b13bf00d..e1c85d8a 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -11,7 +11,7 @@ This is a literate `rzk` file:
 ```rzk
 #assume funext : FunExt
 -- #assume weakextext : WeakExtExt
--- #assume extext : ExtExt
+#assume extext : ExtExt
 ```
 
 ### The 3 dimensional 2-Segal horns
@@ -176,16 +176,16 @@ We use the conventions from the definition of `#!rzk hom3` from
 A type is 2-Segal if and only if its based hom-types are Segal.
 
 ```rzk
-#def test45
-  ( A : U)
-  ( w x y : A)
-  ( f : hom A w x)
-  ( gf : hom A w y)
-  ( g : hom A x y)
-  ( α₃ : hom2 A w x y f g gf)
-  : hom (coslice A w) (x , f) (y , gf)
-  :=
-    U
+-- #def test45
+--   ( A : U)
+--   ( w x y : A)
+--   ( f : hom A w x)
+--   ( gf : hom A w y)
+--   ( g : hom A x y)
+--   ( α₃ : hom2 A w x y f g gf)
+--   : hom (coslice A w) (x , f) (y , gf)
+--   :=
+--     U
 ```
 
 A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
@@ -200,72 +200,148 @@ A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
      ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₁₃₎ A)
 ```
 
-The proof of `is-local-horn-inclusion-function-type` works for 2-segal types by
-just changing the horns.
+The proof of `is-local-horn-inclusion-function-type` generalizes to types being
+local with respect to an arbitrary subshape inclusion.
+
+```rzk
+#def subshape-restriction
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : U)
+  : ( ψ → A) → (ϕ → A)
+  := \ f t → f t
+
+#def is-local-function-type-fiberwise-is-local
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : U)
+  ( C : A → U)
+  ( fiberwise-is-local-C : (x : A) → is-local-type I ψ ϕ (C x))
+  : is-local-type I ψ ϕ ((x : A) → C x)
+  :=
+    is-equiv-triple-comp
+      ( ψ → ((x : A) → C x))
+      ( ( x : A) → ψ → C x)
+      ( ( x : A) → ϕ → C x)
+      ( ϕ → ((x : A) → C x))
+      ( \ g x t → g t x) -- first equivalence
+      ( second (flip-ext-fun
+        ( I)
+        ( ψ)
+        ( \ t → BOT)
+        ( A)
+        ( \ t → C)
+        ( \ t → recBOT)))
+      ( \ h x t → h x t) -- second equivalence
+      ( second (equiv-function-equiv-family
+        ( funext)
+        ( A)
+        ( \ x → (ψ → C x))
+        ( \ x → (ϕ → C x))
+        ( \ x → (subshape-restriction I ψ ϕ (C x) , fiberwise-is-local-C x))))
+      ( \ h t x → (h x) t) -- third equivalence
+      ( second (flip-ext-fun-inv
+        ( I)
+        ( \ t → ϕ t)
+        ( \ t → BOT)
+        ( A)
+        ( \ t → C)
+        ( \ t → recBOT)))
+```
+
+Using this general form, we prove that (dependent) function types into a family
+of 2-Segal types are 2-Segal.
 
 ```rzk
 #def is-local-2-segal-horn-inclusion-function-type uses (funext)
-  ( X : U)
-  ( A : X → U)
-  ( fiberwise-is-2-segal-A : (x : X) → is-local-2-segal-horn-inclusion (A x))
-  : is-local-2-segal-horn-inclusion ((x : X) → A x)
+  ( A : U)
+  ( C : A → U)
+  ( fiberwise-is-2-segal-A : (x : A) → is-local-2-segal-horn-inclusion (C x))
+  : is-local-2-segal-horn-inclusion ((x : A) → C x)
   :=
-    ( ( is-equiv-triple-comp
-        ( Δ³ → ((x : X) → A x))
-        ( ( x : X) → Δ³ → A x)
-        ( ( x : X) → Λ³₍₀₂₎ → A x)
-        ( Λ³₍₀₂₎ → ((x : X) → A x))
-        ( \ g x t → g t x) -- first equivalence
-        ( second (flip-ext-fun
-          ( 2 × 2 × 2)
-          ( Δ³)
+    ( is-local-function-type-fiberwise-is-local
+        ( 2 × 2 × 2)
+        ( Δ³)
+        ( Λ³₍₀₂₎)
+        ( A)
+        ( C)
+        ( \ x → first (fiberwise-is-2-segal-A x))
+    , is-local-function-type-fiberwise-is-local
+        ( 2 × 2 × 2)
+        ( Δ³)
+        ( Λ³₍₁₃₎)
+        ( A)
+        ( C)
+        ( \ x → second (fiberwise-is-2-segal-A x)))
+```
+
+We do the same for the proof of `is-local-horn-inclusion-extension-type`
+
+```rzk
+#def is-local-subshape-inclusion-extension-type uses (extext)
+  ( I J : CUBE)
+  ( χ : I → TOPE)
+  ( ψ : J → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : χ → U)
+  ( fiberwise-is-local-A : (s : χ) → is-local-type J ψ ϕ (A s))
+  : is-local-type J ψ ϕ ((s : χ) → A s)
+  :=
+    is-equiv-triple-comp
+      ( ψ → (s : χ) → A s)
+      ( ( s : χ) → ψ → A s)
+      ( ( s : χ) → ϕ → A s)
+      ( ϕ → (s : χ) → A s)
+      ( \ g s t → g t s)  -- first equivalence
+      ( second
+        ( fubini
+          ( J)
+          ( I)
+          ( \ t → ψ t)
           ( \ t → BOT)
-          ( X)
-          ( \ t → A)
-          ( \ t → recBOT)))
-        ( \ h x t → h x t) -- second equivalence
-        ( second (equiv-function-equiv-family
-          ( funext)
-          ( X)
-          ( \ x → (Δ³ → A x))
-          ( \ x → (Λ³₍₀₂₎ → A x))
-          ( \ x → (3-horn-restriction₍₀₂₎ (A x)
-            , first (fiberwise-is-2-segal-A x)))))
-        ( \ h t x → (h x) t) -- third equivalence
-        ( second (flip-ext-fun-inv
-          ( 2 × 2 × 2)
-          ( \ t → Λ³₍₀₂₎ t)
+          ( χ)
+          ( \ s → BOT)
+          ( \ t s → A s)
+          ( \ u → recBOT)))
+      ( \ h s t → h s t) -- second equivalence
+      ( second (equiv-extensions-equiv extext I χ (\ _ → BOT)
+        ( \ s → ψ → A s)
+        ( \ s → ϕ → A s)
+        ( \ s → (subshape-restriction J ψ ϕ (A s) , fiberwise-is-local-A s))
+        ( \ _ → recBOT)))
+      ( \ h t s → (h s) t) -- third equivalence
+      ( second
+        ( fubini
+          ( I)
+          ( J)
+          ( χ)
+          ( \ s → BOT)
+          ( \ t → ϕ t)
           ( \ t → BOT)
-          ( X)
-          ( \ t → A)
-          ( \ t → recBOT))))
-          , ( is-equiv-triple-comp
-              ( Δ³ → ((x : X) → A x))
-              ( ( x : X) → Δ³ → A x)
-              ( ( x : X) → Λ³₍₁₃₎ → A x)
-              ( Λ³₍₁₃₎ → ((x : X) → A x))
-              ( \ g x t → g t x) -- first equivalence
-              ( second (flip-ext-fun
-                ( 2 × 2 × 2)
-                ( Δ³)
-                ( \ t → BOT)
-                ( X)
-                ( \ t → A)
-                ( \ t → recBOT)))
-              ( \ h x t → h x t) -- second equivalence
-              ( second (equiv-function-equiv-family
-                ( funext)
-                ( X)
-                ( \ x → (Δ³ → A x))
-                ( \ x → (Λ³₍₁₃₎ → A x))
-                ( \ x → (3-horn-restriction₍₁₃₎ (A x)
-                  , second (fiberwise-is-2-segal-A x)))))
-              ( \ h t x → (h x) t) -- third equivalence
-              ( second (flip-ext-fun-inv
-                ( 2 × 2 × 2)
-                ( \ t → Λ³₍₁₃₎ t)
-                ( \ t → BOT)
-                ( X)
-                ( \ t → A)
-                ( \ t → recBOT)))))
+          ( \ s t → A s)
+          ( \ u → recBOT)))
+
+#def is-2-segal-extension-type uses (extext)
+  ( I : CUBE)
+  ( χ : I → TOPE)
+  ( A : χ → U)
+  ( fiberwise-is-2-segal-A : (s : χ) → is-local-2-segal-horn-inclusion (A s))
+  : is-local-2-segal-horn-inclusion ((s : χ) → A s)
+  :=
+    ( is-local-subshape-inclusion-extension-type I
+        ( 2 × 2 × 2)
+        ( χ)
+        ( Δ³)
+        ( Λ³₍₀₂₎)
+        ( A)
+        ( \ x → first (fiberwise-is-2-segal-A x))
+    , is-local-subshape-inclusion-extension-type I
+        ( 2 × 2 × 2)
+        ( χ)
+        ( Δ³)
+        ( Λ³₍₁₃₎)
+        ( A)
+        ( \ x → second (fiberwise-is-2-segal-A x)))
 ```

From 27e74e2d529bf37bf46f135e2e4fc284cc59932e Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Tue, 30 Jul 2024 12:10:19 +0200
Subject: [PATCH 8/9] horror

---
 src/2Segal/2segal-types.rzk.md            | 96 +++++++++++++++++++++++
 src/simplicial-hott/05-segal-types.rzk.md |  2 +-
 2 files changed, 97 insertions(+), 1 deletion(-)

diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
index e1c85d8a..b3a49cf1 100644
--- a/src/2Segal/2segal-types.rzk.md
+++ b/src/2Segal/2segal-types.rzk.md
@@ -198,6 +198,102 @@ A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
     product
      ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₀₂₎ A)
      ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₁₃₎ A)
+
+#def equiv-2-segal-horn-restriction₍₀₂₎
+  ( A : U)
+  : Equiv
+    ( Δ³ → A)
+    ( Σ ( k : Λ³₍₀₂₎ → A)
+      , ( Σ ( hg : hom A (k ((1₂ , 0₂) , 0₂)) (k ((1₂ , 1₂) , 1₂)))
+          , ( Σ ( α₂ : hom2
+                        ( A)
+                        ( k ((0₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 1₂))
+                        ( \ t → k ((t , 0₂) , 0₂))
+                        ( hg)
+                        ( \ t → k ((t , t) , t)))
+              , ( Σ ( α₀ : hom2
+                            ( A)
+                            ( k ((1₂ , 0₂) , 0₂))
+                            ( k ((1₂ , 1₂) , 0₂))
+                            ( k ((1₂ , 1₂) , 1₂))
+                            ( \ t → k ((1₂ , t) , 0₂))
+                            ( \ t → k ((1₂ , 1₂) , t))
+                            ( hg))
+                  , ( hom3
+                        ( A)
+                        ( k ((0₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 1₂))
+                        ( \ t → k ((t , 0₂) , 0₂))
+                        ( \ t → k ((t , t) , 0₂))
+                        ( \ t → k ((t , t) , t))
+                        ( \ t → k ((1₂ , t) , 0₂))
+                        ( hg)
+                        ( \ t → k ((1₂ , 1₂) , t))
+                        ( \ (t , s) → k ((t , s) , 0₂))
+                        ( α₂)
+                        ( \ (t , s) → k ((t , t) , s))
+                        ( α₀))))))
+  :=
+    ( \ H →
+      ( ( ( ( ( \ t → H t)
+        , ( ( ( \ t → H ((1₂ , t) , t))
+          , ( ( ( \ (t , s) → H ((t , s) , s))
+            , ( ( \ (t , s) → H ((1₂ , t) , s)
+              , ( H)))))))))))
+      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl)
+      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl))))
+
+#def equiv-2-segal-horn-restriction₍₁₃₎
+  ( A : U)
+  : Equiv
+    ( Δ³ → A)
+    ( Σ ( k : Λ³₍₁₃₎ → A)
+      , ( Σ ( gf : hom A (k ((0₂ , 0₂) , 0₂)) (k ((1₂ , 1₂) , 0₂)))
+          , ( Σ ( α₃ : hom2
+                        ( A)
+                        ( k ((0₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 0₂))
+                        ( \ t → k ((t , 0₂) , 0₂))
+                        ( \ t → k ((1₂ , t) , 0₂))
+                        ( gf))
+              , ( Σ ( α₁ : hom2
+                            ( A)
+                            ( k ((0₂ , 0₂) , 0₂))
+                            ( k ((1₂ , 1₂) , 0₂))
+                            ( k ((1₂ , 1₂) , 1₂))
+                            ( gf)
+                            ( \ t → k ((1₂ , 1₂) , t))
+                            ( \ t → k ((t , t) , t)))
+                  , ( hom3
+                        ( A)
+                        ( k ((0₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 0₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 0₂))
+                        ( k ((1₂ , 1₂) , 1₂))
+                        ( \ t → k ((t , 0₂) , 0₂))
+                        ( gf)
+                        ( \ t → k ((t , t) , t))
+                        ( \ t → k ((1₂ , t) , 0₂))
+                        ( \ t → k ((1₂ , t) , t))
+                        ( \ t → k ((1₂ , 1₂) , t))
+                        ( α₃)
+                        ( \ (t , s) → k ((t , s) , s))
+                        ( α₁)
+                        ( \ (t , s) → k ((1₂ , t) , s)))))))
+  :=
+    ( \ H →
+      ( ( ( ( ( \ t → H t)
+        , ( ( ( \ t → H ((t , t) , 0₂))
+          , ( ( ( \ (t , s) → H ((t , s) , 0₂))
+            , ( ( \ (t , s) → H ((t , t) , s)
+              , ( H)))))))))))
+      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl)
+      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl))))
 ```
 
 The proof of `is-local-horn-inclusion-function-type` generalizes to types being
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index d78d0e77..bda65246 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -487,7 +487,7 @@ witnesses of the equivalence).
               ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
               ( \ t → k (t , 0₂)) (\ t → k (1₂ , t))
               ( h)))
-    , ( is-equiv-projection-contractible-fibers
+      , ( is-equiv-projection-contractible-fibers
           ( Λ → A)
           ( \ k →
             Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))

From eb7fe775c60af31700912d746a15a6e99ce5b1f2 Mon Sep 17 00:00:00 2001
From: Theofanis Chatzidiamantis-Christoforidis <thchatzidiamantis@gmail.com>
Date: Tue, 30 Jul 2024 12:47:55 +0200
Subject: [PATCH 9/9] function types into local families

---
 rzk.yaml                                      |   1 -
 src/2Segal/2segal-types.rzk.md                | 443 ------------------
 .../04-right-orthogonal.rzk.md                | 102 ++++
 src/simplicial-hott/05-segal-types.rzk.md     |  78 +--
 4 files changed, 119 insertions(+), 505 deletions(-)
 delete mode 100644 src/2Segal/2segal-types.rzk.md

diff --git a/rzk.yaml b/rzk.yaml
index b7e9efdf..4c2fc69f 100644
--- a/rzk.yaml
+++ b/rzk.yaml
@@ -1,4 +1,3 @@
 include:
   - src/hott/**/*.rzk.md
   - src/simplicial-hott/**/*.rzk.md
-  - src/2Segal/**/*.rzk.md
diff --git a/src/2Segal/2segal-types.rzk.md b/src/2Segal/2segal-types.rzk.md
deleted file mode 100644
index b3a49cf1..00000000
--- a/src/2Segal/2segal-types.rzk.md
+++ /dev/null
@@ -1,443 +0,0 @@
-# 2-Segal spaces
-
-Experimental formalization project on 2-Segal spaces.
-
-This is a literate `rzk` file:
-
-```rzk
-#lang rzk-1
-```
-
-```rzk
-#assume funext : FunExt
--- #assume weakextext : WeakExtExt
-#assume extext : ExtExt
-```
-
-### The 3 dimensional 2-Segal horns
-
-```rzk
-#def Λ³₍₀₂₎
-  : Δ³ → TOPE
-  :=
-    \ ((t1 , t2) , t3) → t3 ≡ 0₂ ∨ t1 ≡ t2 -- This could be t3==t2.
-
-#def Λ³₍₁₃₎
-  : Δ³ → TOPE
-  :=
-    \ ((t1 , t2) , t3) → t2 ≡ t3 ∨ t1 ≡ 1₂ -- This could be t1==t2.
-
-#def 3-horn-restriction₍₀₂₎
-  ( A : U)
-  : ( Δ³ → A) → (Λ³₍₀₂₎ → A)
-  := \ f t → f t
-
-#def 3-horn-restriction₍₁₃₎
-  ( A : U)
-  : ( Δ³ → A) → (Λ³₍₁₃₎ → A)
-  := \ f t → f t
-```
-
-### 2-Segal types
-
-We use the conventions from the definition of `#!rzk hom3` from
-`11-adjunctions.rzk`.
-
-```rzk
-#def is-2-segal₍₀₂₎
-  ( A : U)
-  : U
-  :=
-    ( w : A) → (x : A) → (y : A) → (z : A)
-  → ( f : hom A w x) → (gf : hom A w y) → (hgf : hom A w z)
-  → ( g : hom A x y) → (h : hom A y z)
-  → ( α₃ : hom2 A w x y f g gf) → (α₁ : hom2 A w y z gf h hgf)
-  → is-contr
-      ( Σ ( hg : hom A x z)
-      , ( Σ ( α₂ : hom2 A w x z f hg hgf)
-        , ( Σ ( α₀ : hom2 A x y z g h hg)
-            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
-
-#def is-2-segal₍₁₃₎
-  ( A : U)
-  : U
-  :=
-    ( w : A) → (x : A) → (y : A) → (z : A)
-  → ( f : hom A w x) → (hgf : hom A w z)
-  → ( g : hom A x y) → (hg : hom A x z) → (h : hom A y z)
-  → ( α₂ : hom2 A w x z f hg hgf) → (α₀ : hom2 A x y z g h hg)
-  → is-contr
-      ( Σ ( gf : hom A w y)
-      , ( Σ ( α₃ : hom2 A w x y f g gf)
-        , ( Σ ( α₁ : hom2 A w y z gf h hgf)
-            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
-
-#def is-2-segal
-  ( A : U)
-  : U
-  :=
-    product (is-2-segal₍₀₂₎ A) (is-2-segal₍₁₃₎ A)
-```
-
-```rzk
-#def 3horn₍₀₂₎
-  ( A : U)
-  ( w x y z : A)
-  ( f : hom A w x)
-  ( gf : hom A w y)
-  ( hgf : hom A w z)
-  ( g : hom A x y)
-  ( h : hom A y z)
-  ( α₃ : hom2 A w x y f g gf)
-  ( α₁ : hom2 A w y z gf h hgf)
-  : Λ³₍₀₂₎ → A
-  :=
-    \ ((t₁ , t₂) , t₃) →
-      recOR
-        ( t₃ ≡ 0₂ ↦ α₃ (t₁ , t₂)
-        , t₁ ≡ t₂ ↦ α₁ (t₁ , t₃)) -- This could be t3==t2.
-
-#def 3horn₍₁₃₎
-  ( A : U)
-  ( w x y z : A)
-  ( f : hom A w x)
-  ( hgf : hom A w z)
-  ( g : hom A x y)
-  ( hg : hom A x z)
-  ( h : hom A y z)
-  ( α₂ : hom2 A w x z f hg hgf)
-  ( α₀ : hom2 A x y z g h hg)
-  : Λ³₍₁₃₎ → A
-  :=
-  \ ((t₁ , t₂) , t₃) →
-    recOR
-      ( t₂ ≡ t₃ ↦ α₂ (t₁ , t₃) -- This could be t1==t2.
-      , t₁ ≡ 1₂ ↦ α₀ (t₂ , t₃))
-
-#def associators-are-3horn-fillings₍₀₂₎
-  ( A : U)
-  ( w x y z : A)
-  ( f : hom A w x)
-  ( gf : hom A w y)
-  ( hgf : hom A w z)
-  ( g : hom A x y)
-  ( h : hom A y z)
-  ( α₃ : hom2 A w x y f g gf)
-  ( α₁ : hom2 A w y z gf h hgf)
-  : Equiv
-      ( Σ ( hg : hom A x z)
-      , ( Σ ( α₂ : hom2 A w x z f hg hgf)
-        , ( Σ ( α₀ : hom2 A x y z g h hg)
-            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
-      ( ( t : Δ³) → A [Λ³₍₀₂₎ t ↦ 3horn₍₀₂₎ A w x y z f gf hgf g h α₃ α₁ t])
-  :=
-    ( \ H t → second (second (second H)) t
-      , ( ( ( \ k → (\ t → k ((1₂ , t) , t)
-          , ( \ (t , s) → k ((t , s) , s)
-            , ( \ (t , s) → k ((1₂ , t) , s)
-              , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
-          , \ H → refl))
-        , ( ( \ k → (\ t → k ((1₂ , t) , t)
-            , ( \ (t , s) → k ((t , s) , s)
-              , ( \ (t , s) → k ((1₂ , t) , s)
-                , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
-            , \ H → refl))))
-
-#def associators-are-3horn-fillings₍₁₃₎
-  ( A : U)
-  ( w x y z : A)
-  ( f : hom A w x)
-  ( hgf : hom A w z)
-  ( g : hom A x y)
-  ( hg : hom A x z)
-  ( h : hom A y z)
-  ( α₂ : hom2 A w x z f hg hgf)
-  ( α₀ : hom2 A x y z g h hg)
-  : Equiv
-      ( Σ ( gf : hom A w y)
-      , ( Σ ( α₃ : hom2 A w x y f g gf)
-        , ( Σ ( α₁ : hom2 A w y z gf h hgf)
-            , hom3 A w x y z f gf hgf g hg h α₃ α₂ α₁ α₀)))
-      ( ( t : Δ³) → A [Λ³₍₁₃₎ t ↦ 3horn₍₁₃₎ A w x y z f hgf g hg h α₂ α₀ t])
-  :=
-    ( \ H t → second (second (second H)) t
-      , ( ( ( \ k → (\ t → k ((t , t) , 0₂)
-          , ( \ (t , s) → k ((t , s) , 0₂)
-            , ( \ (t , s) → k ((t , t) , s)
-              , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
-          , \ H → refl))
-        , ( ( \ k → (\ t → k ((t , t) , 0₂)
-            , ( \ (t , s) → k ((t , s) , 0₂)
-              , ( \ (t , s) → k ((t , t) , s)
-                , \ ((t1 , t2) , t3) → k ((t1 , t2) , t3))))
-            , \ H → refl))))
-```
-
-A type is 2-Segal if and only if its based hom-types are Segal.
-
-```rzk
--- #def test45
---   ( A : U)
---   ( w x y : A)
---   ( f : hom A w x)
---   ( gf : hom A w y)
---   ( g : hom A x y)
---   ( α₃ : hom2 A w x y f g gf)
---   : hom (coslice A w) (x , f) (y , gf)
---   :=
---     U
-```
-
-A type is 2-Segal iff it is local with respect to 2-Segal horn inclusions.
-
-```rzk
-#def is-local-2-segal-horn-inclusion
-  ( A : U)
-  : U
-  :=
-    product
-     ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₀₂₎ A)
-     ( is-local-type (2 × 2 × 2) Δ³ Λ³₍₁₃₎ A)
-
-#def equiv-2-segal-horn-restriction₍₀₂₎
-  ( A : U)
-  : Equiv
-    ( Δ³ → A)
-    ( Σ ( k : Λ³₍₀₂₎ → A)
-      , ( Σ ( hg : hom A (k ((1₂ , 0₂) , 0₂)) (k ((1₂ , 1₂) , 1₂)))
-          , ( Σ ( α₂ : hom2
-                        ( A)
-                        ( k ((0₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 1₂))
-                        ( \ t → k ((t , 0₂) , 0₂))
-                        ( hg)
-                        ( \ t → k ((t , t) , t)))
-              , ( Σ ( α₀ : hom2
-                            ( A)
-                            ( k ((1₂ , 0₂) , 0₂))
-                            ( k ((1₂ , 1₂) , 0₂))
-                            ( k ((1₂ , 1₂) , 1₂))
-                            ( \ t → k ((1₂ , t) , 0₂))
-                            ( \ t → k ((1₂ , 1₂) , t))
-                            ( hg))
-                  , ( hom3
-                        ( A)
-                        ( k ((0₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 1₂))
-                        ( \ t → k ((t , 0₂) , 0₂))
-                        ( \ t → k ((t , t) , 0₂))
-                        ( \ t → k ((t , t) , t))
-                        ( \ t → k ((1₂ , t) , 0₂))
-                        ( hg)
-                        ( \ t → k ((1₂ , 1₂) , t))
-                        ( \ (t , s) → k ((t , s) , 0₂))
-                        ( α₂)
-                        ( \ (t , s) → k ((t , t) , s))
-                        ( α₀))))))
-  :=
-    ( \ H →
-      ( ( ( ( ( \ t → H t)
-        , ( ( ( \ t → H ((1₂ , t) , t))
-          , ( ( ( \ (t , s) → H ((t , s) , s))
-            , ( ( \ (t , s) → H ((1₂ , t) , s)
-              , ( H)))))))))))
-      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl)
-      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl))))
-
-#def equiv-2-segal-horn-restriction₍₁₃₎
-  ( A : U)
-  : Equiv
-    ( Δ³ → A)
-    ( Σ ( k : Λ³₍₁₃₎ → A)
-      , ( Σ ( gf : hom A (k ((0₂ , 0₂) , 0₂)) (k ((1₂ , 1₂) , 0₂)))
-          , ( Σ ( α₃ : hom2
-                        ( A)
-                        ( k ((0₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 0₂))
-                        ( \ t → k ((t , 0₂) , 0₂))
-                        ( \ t → k ((1₂ , t) , 0₂))
-                        ( gf))
-              , ( Σ ( α₁ : hom2
-                            ( A)
-                            ( k ((0₂ , 0₂) , 0₂))
-                            ( k ((1₂ , 1₂) , 0₂))
-                            ( k ((1₂ , 1₂) , 1₂))
-                            ( gf)
-                            ( \ t → k ((1₂ , 1₂) , t))
-                            ( \ t → k ((t , t) , t)))
-                  , ( hom3
-                        ( A)
-                        ( k ((0₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 0₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 0₂))
-                        ( k ((1₂ , 1₂) , 1₂))
-                        ( \ t → k ((t , 0₂) , 0₂))
-                        ( gf)
-                        ( \ t → k ((t , t) , t))
-                        ( \ t → k ((1₂ , t) , 0₂))
-                        ( \ t → k ((1₂ , t) , t))
-                        ( \ t → k ((1₂ , 1₂) , t))
-                        ( α₃)
-                        ( \ (t , s) → k ((t , s) , s))
-                        ( α₁)
-                        ( \ (t , s) → k ((1₂ , t) , s)))))))
-  :=
-    ( \ H →
-      ( ( ( ( ( \ t → H t)
-        , ( ( ( \ t → H ((t , t) , 0₂))
-          , ( ( ( \ (t , s) → H ((t , s) , 0₂))
-            , ( ( \ (t , s) → H ((t , t) , s)
-              , ( H)))))))))))
-      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl)
-      , ( ( \ G t → second (second (second (second (G)))) t , \ H → refl))))
-```
-
-The proof of `is-local-horn-inclusion-function-type` generalizes to types being
-local with respect to an arbitrary subshape inclusion.
-
-```rzk
-#def subshape-restriction
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : U)
-  : ( ψ → A) → (ϕ → A)
-  := \ f t → f t
-
-#def is-local-function-type-fiberwise-is-local
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : U)
-  ( C : A → U)
-  ( fiberwise-is-local-C : (x : A) → is-local-type I ψ ϕ (C x))
-  : is-local-type I ψ ϕ ((x : A) → C x)
-  :=
-    is-equiv-triple-comp
-      ( ψ → ((x : A) → C x))
-      ( ( x : A) → ψ → C x)
-      ( ( x : A) → ϕ → C x)
-      ( ϕ → ((x : A) → C x))
-      ( \ g x t → g t x) -- first equivalence
-      ( second (flip-ext-fun
-        ( I)
-        ( ψ)
-        ( \ t → BOT)
-        ( A)
-        ( \ t → C)
-        ( \ t → recBOT)))
-      ( \ h x t → h x t) -- second equivalence
-      ( second (equiv-function-equiv-family
-        ( funext)
-        ( A)
-        ( \ x → (ψ → C x))
-        ( \ x → (ϕ → C x))
-        ( \ x → (subshape-restriction I ψ ϕ (C x) , fiberwise-is-local-C x))))
-      ( \ h t x → (h x) t) -- third equivalence
-      ( second (flip-ext-fun-inv
-        ( I)
-        ( \ t → ϕ t)
-        ( \ t → BOT)
-        ( A)
-        ( \ t → C)
-        ( \ t → recBOT)))
-```
-
-Using this general form, we prove that (dependent) function types into a family
-of 2-Segal types are 2-Segal.
-
-```rzk
-#def is-local-2-segal-horn-inclusion-function-type uses (funext)
-  ( A : U)
-  ( C : A → U)
-  ( fiberwise-is-2-segal-A : (x : A) → is-local-2-segal-horn-inclusion (C x))
-  : is-local-2-segal-horn-inclusion ((x : A) → C x)
-  :=
-    ( is-local-function-type-fiberwise-is-local
-        ( 2 × 2 × 2)
-        ( Δ³)
-        ( Λ³₍₀₂₎)
-        ( A)
-        ( C)
-        ( \ x → first (fiberwise-is-2-segal-A x))
-    , is-local-function-type-fiberwise-is-local
-        ( 2 × 2 × 2)
-        ( Δ³)
-        ( Λ³₍₁₃₎)
-        ( A)
-        ( C)
-        ( \ x → second (fiberwise-is-2-segal-A x)))
-```
-
-We do the same for the proof of `is-local-horn-inclusion-extension-type`
-
-```rzk
-#def is-local-subshape-inclusion-extension-type uses (extext)
-  ( I J : CUBE)
-  ( χ : I → TOPE)
-  ( ψ : J → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : χ → U)
-  ( fiberwise-is-local-A : (s : χ) → is-local-type J ψ ϕ (A s))
-  : is-local-type J ψ ϕ ((s : χ) → A s)
-  :=
-    is-equiv-triple-comp
-      ( ψ → (s : χ) → A s)
-      ( ( s : χ) → ψ → A s)
-      ( ( s : χ) → ϕ → A s)
-      ( ϕ → (s : χ) → A s)
-      ( \ g s t → g t s)  -- first equivalence
-      ( second
-        ( fubini
-          ( J)
-          ( I)
-          ( \ t → ψ t)
-          ( \ t → BOT)
-          ( χ)
-          ( \ s → BOT)
-          ( \ t s → A s)
-          ( \ u → recBOT)))
-      ( \ h s t → h s t) -- second equivalence
-      ( second (equiv-extensions-equiv extext I χ (\ _ → BOT)
-        ( \ s → ψ → A s)
-        ( \ s → ϕ → A s)
-        ( \ s → (subshape-restriction J ψ ϕ (A s) , fiberwise-is-local-A s))
-        ( \ _ → recBOT)))
-      ( \ h t s → (h s) t) -- third equivalence
-      ( second
-        ( fubini
-          ( I)
-          ( J)
-          ( χ)
-          ( \ s → BOT)
-          ( \ t → ϕ t)
-          ( \ t → BOT)
-          ( \ s t → A s)
-          ( \ u → recBOT)))
-
-#def is-2-segal-extension-type uses (extext)
-  ( I : CUBE)
-  ( χ : I → TOPE)
-  ( A : χ → U)
-  ( fiberwise-is-2-segal-A : (s : χ) → is-local-2-segal-horn-inclusion (A s))
-  : is-local-2-segal-horn-inclusion ((s : χ) → A s)
-  :=
-    ( is-local-subshape-inclusion-extension-type I
-        ( 2 × 2 × 2)
-        ( χ)
-        ( Δ³)
-        ( Λ³₍₀₂₎)
-        ( A)
-        ( \ x → first (fiberwise-is-2-segal-A x))
-    , is-local-subshape-inclusion-extension-type I
-        ( 2 × 2 × 2)
-        ( χ)
-        ( Δ³)
-        ( Λ³₍₁₃₎)
-        ( A)
-        ( \ x → second (fiberwise-is-2-segal-A x)))
-```
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 8b9f3e20..9cfc4cb6 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -1060,6 +1060,108 @@ of the restriction map `(ψ → A) → (ϕ → A)`.
 #end has-unique-extensions
 ```
 
+### Function types into fiberwise local families are local
+
+We prove that if $A$ is a type and $C : A → U$ is such that every fiber $C (x)$
+is local with respect to a subshape inclusion, then so is $(x : X) → A (x)$.
+This generalizes the proof of (RS17, Corollary 5.6).
+
+```rzk
+#def subshape-restriction
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : U)
+  : ( ψ → A) → (ϕ → A)
+  := \ f t → f t
+
+#def is-local-function-type-fiberwise-is-local uses (funext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : U)
+  ( C : A → U)
+  ( fiberwise-is-local-C : (x : A) → (is-local-type I ψ ϕ (C x)))
+  : is-local-type I ψ ϕ ((x : A) → C x)
+  :=
+    is-equiv-triple-comp
+      ( ψ → ((x : A) → C x))
+      ( ( x : A) → ψ → C x)
+      ( ( x : A) → ϕ → C x)
+      ( ϕ → ((x : A) → C x))
+      ( \ g x t → g t x) -- first equivalence
+      ( second (flip-ext-fun
+        ( I)
+        ( ψ)
+        ( \ t → BOT)
+        ( A)
+        ( \ t → C)
+        ( \ t → recBOT)))
+      ( \ h x t → h x t) -- second equivalence
+      ( second (equiv-function-equiv-family
+        ( funext)
+        ( A)
+        ( \ x → (ψ → C x))
+        ( \ x → (ϕ → C x))
+        ( \ x → (subshape-restriction I ψ ϕ (C x) , fiberwise-is-local-C x))))
+      ( \ h t x → (h x) t) -- third equivalence
+      ( second (flip-ext-fun-inv
+        ( I)
+        ( \ t → ϕ t)
+        ( \ t → BOT)
+        ( A)
+        ( \ t → C)
+        ( \ t → recBOT)))
+```
+
+We can prove the same thing when $X$ is a shape and $C : X → U$ is fiberwise
+local.
+
+```rzk
+#def is-local-subshape-inclusion-extension-type uses (extext)
+  ( I J : CUBE)
+  ( χ : I → TOPE)
+  ( ψ : J → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A : χ → U)
+  ( fiberwise-is-local-A : (s : χ) → is-local-type J ψ ϕ (A s))
+  : is-local-type J ψ ϕ ((s : χ) → A s)
+  :=
+    is-equiv-triple-comp
+      ( ψ → (s : χ) → A s)
+      ( ( s : χ) → ψ → A s)
+      ( ( s : χ) → ϕ → A s)
+      ( ϕ → (s : χ) → A s)
+      ( \ g s t → g t s)  -- first equivalence
+      ( second
+        ( fubini
+          ( J)
+          ( I)
+          ( \ t → ψ t)
+          ( \ t → BOT)
+          ( χ)
+          ( \ s → BOT)
+          ( \ t s → A s)
+          ( \ u → recBOT)))
+      ( \ h s t → h s t) -- second equivalence
+      ( second (equiv-extensions-equiv extext I χ (\ _ → BOT)
+        ( \ s → ψ → A s)
+        ( \ s → ϕ → A s)
+        ( \ s → (subshape-restriction J ψ ϕ (A s) , fiberwise-is-local-A s))
+        ( \ _ → recBOT)))
+      ( \ h t s → (h s) t) -- third equivalence
+      ( second
+        ( fubini
+          ( I)
+          ( J)
+          ( χ)
+          ( \ s → BOT)
+          ( \ t → ϕ t)
+          ( \ t → BOT)
+          ( \ s t → A s)
+          ( \ u → recBOT)))
+```
+
 ### Properties of local types / unique extension types
 
 We fix a shape inclusion `ϕ ⊂ ψ`.
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index bda65246..ff4fb933 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -606,34 +606,14 @@ all $x$ then $(x : X) → A x$ is a Segal type.
   ( fiberwise-is-segal-A : (x : X) → is-local-horn-inclusion (A x))
   : is-local-horn-inclusion ((x : X) → A x)
   :=
-    is-equiv-triple-comp
-      ( Δ² → ((x : X) → A x))
-      ( ( x : X) → Δ² → A x)
-      ( ( x : X) → Λ → A x)
-      ( Λ → ((x : X) → A x))
-      ( \ g x t → g t x) -- first equivalence
-      ( second (flip-ext-fun
-        ( 2 × 2)
-        ( Δ²)
-        ( \ t → BOT)
-        ( X)
-        ( \ t → A)
-        ( \ t → recBOT)))
-      ( \ h x t → h x t) -- second equivalence
-      ( second (equiv-function-equiv-family
-        ( funext)
-        ( X)
-        ( \ x → (Δ² → A x))
-        ( \ x → (Λ → A x))
-        ( \ x → (horn-restriction (A x) , fiberwise-is-segal-A x))))
-      ( \ h t x → (h x) t) -- third equivalence
-      ( second (flip-ext-fun-inv
-        ( 2 × 2)
-        ( Λ)
-        ( \ t → BOT)
-        ( X)
-        ( \ t → A)
-        ( \ t → recBOT)))
+    is-local-function-type-fiberwise-is-local
+      ( funext)
+      ( 2 × 2)
+      ( Δ²)
+      ( \ t → Λ t)
+      ( X)
+      ( A)
+      ( fiberwise-is-segal-A)
 
 #def is-segal-function-type uses (funext)
   ( X : U)
@@ -659,39 +639,15 @@ then $(x : X) → A x$ is a Segal type.
   ( fiberwise-is-segal-A : (s : ψ) → is-local-horn-inclusion (A s))
   : is-local-horn-inclusion ((s : ψ) → A s)
   :=
-    is-equiv-triple-comp
-      ( Δ² → (s : ψ) → A s)
-      ( ( s : ψ) → Δ² → A s)
-      ( ( s : ψ) → Λ → A s)
-      ( Λ → (s : ψ) → A s)
-      ( \ g s t → g t s)  -- first equivalence
-      ( second
-        ( fubini
-          ( 2 × 2)
-          ( I)
-          ( Δ²)
-          ( \ t → BOT)
-          ( ψ)
-          ( \ s → BOT)
-          ( \ t s → A s)
-          ( \ u → recBOT)))
-      ( \ h s t → h s t) -- second equivalence
-      ( second (equiv-extensions-equiv extext I ψ (\ _ → BOT)
-        ( \ s → Δ² → A s)
-        ( \ s → Λ → A s)
-        ( \ s → (horn-restriction (A s) , fiberwise-is-segal-A s))
-        ( \ _ → recBOT)))
-      ( \ h t s → (h s) t) -- third equivalence
-      ( second
-        ( fubini
-          ( I)
-          ( 2 × 2)
-          ( ψ)
-          ( \ s → BOT)
-          ( Λ)
-          ( \ t → BOT)
-          ( \ s t → A s)
-          ( \ u → recBOT)))
+    is-local-subshape-inclusion-extension-type
+      ( extext)
+      ( I)
+      ( 2 × 2)
+      ( ψ)
+      ( Δ²)
+      ( \ t → Λ t)
+      ( A)
+      ( fiberwise-is-segal-A)
 
 #def is-segal-extension-type uses (extext)
   ( I : CUBE)