Generalized proofs of [RS17, Cor. 5.6]

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 `ϕ ⊂ ψ`.

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₂)))
@@ -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)