FrozenWinters · January 11, 2023 20:24 · Jan 11, 2023
diff --git a/B.agda b/B.agda
@@ -0,0 +1,497 @@
+{-# OPTIONS --cubical --guardedness --rewriting #-}
+
+module B where
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public
+open import Cubical.Core.Everything public
+open import Cubical.Foundations.Everything renaming (cong to ap) public
+
+{-# BUILTIN REWRITE _≡_ #-}
+
+-- Definition of a B-system
+
+private
+  variable
+    ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ ℓ₈ : Level
+
+record Frame ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
+  coinductive
+  field
+    𝑡𝑦 : Type ℓ₁
+    𝑒𝑙 : 𝑡𝑦 → Type ℓ₂
+    𝑒𝑥 : 𝑡𝑦 → Frame ℓ₁ ℓ₂
+
+open Frame public
+
+record FrameMor (𝔸 : Frame ℓ₁ ℓ₂) (𝔹 : Frame ℓ₃ ℓ₄)
+       : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+  coinductive
+  field
+    𝑓𝑢𝑛₀ : 𝑡𝑦 𝔸 → 𝑡𝑦 𝔹
+    𝑓𝑢𝑛₁ : {A : 𝑡𝑦 𝔸} → 𝑒𝑙 𝔸 A → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ A)
+    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → FrameMor (𝑒𝑥 𝔸 A) (𝑒𝑥 𝔹 (𝑓𝑢𝑛₀ A))
+
+open FrameMor public
+
+infixl 20 _∘FM_
+_∘FM_ : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆} →
+  FrameMor 𝔹 ℂ → FrameMor 𝔸 𝔹 → FrameMor 𝔸 ℂ
+𝑓𝑢𝑛₀ (𝑓 ∘FM 𝑔) = 𝑓𝑢𝑛₀ 𝑓 ∘ 𝑓𝑢𝑛₀ 𝑔
+𝑓𝑢𝑛₁ (𝑓 ∘FM 𝑔) = 𝑓𝑢𝑛₁ 𝑓 ∘ 𝑓𝑢𝑛₁ 𝑔
+𝑢𝑝 (𝑓 ∘FM 𝑔) A = 𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A) ∘FM 𝑢𝑝 𝑔 A
+
+∘FM-Assoc : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄}
+  {ℂ : Frame ℓ₅ ℓ₆} {𝔻 : Frame ℓ₇ ℓ₈}
+  (𝑓 : FrameMor ℂ 𝔻) (𝑔 : FrameMor 𝔹 ℂ) (ℎ : FrameMor 𝔸 𝔹) →
+  (𝑓 ∘FM 𝑔) ∘FM ℎ ≡ 𝑓 ∘FM (𝑔 ∘FM ℎ)
+𝑓𝑢𝑛₀ (∘FM-Assoc 𝑓 𝑔 ℎ i) A = 𝑓𝑢𝑛₀ 𝑓 (𝑓𝑢𝑛₀ 𝑔 (𝑓𝑢𝑛₀ ℎ A))
+𝑓𝑢𝑛₁ (∘FM-Assoc 𝑓 𝑔 ℎ i) t = 𝑓𝑢𝑛₁ 𝑓 (𝑓𝑢𝑛₁ 𝑔 (𝑓𝑢𝑛₁ ℎ t))
+𝑢𝑝 (∘FM-Assoc 𝑓 𝑔 ℎ i) A =
+  ∘FM-Assoc (𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 (𝑓𝑢𝑛₀ ℎ A))) (𝑢𝑝 𝑔 (𝑓𝑢𝑛₀ ℎ A)) (𝑢𝑝 ℎ A) i
+
+{-# REWRITE ∘FM-Assoc #-}
+
+idFM : (𝔸 : Frame ℓ₁ ℓ₂) → FrameMor 𝔸 𝔸
+𝑓𝑢𝑛₀ (idFM 𝔸) A = A
+𝑓𝑢𝑛₁ (idFM 𝔸) t = t
+𝑢𝑝 (idFM 𝔸) A = idFM (𝑒𝑥 𝔸 A)
+
+idFM-L : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} (𝑓 : FrameMor 𝔸 𝔹) →
+  idFM 𝔹 ∘FM 𝑓 ≡ 𝑓
+𝑓𝑢𝑛₀ (idFM-L 𝑓 i) A = 𝑓𝑢𝑛₀ 𝑓 A
+𝑓𝑢𝑛₁ (idFM-L 𝑓 i) t = 𝑓𝑢𝑛₁ 𝑓 t
+𝑢𝑝 (idFM-L 𝑓 i) A = idFM-L (𝑢𝑝 𝑓 A) i
+
+idFM-R : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} (𝑓 : FrameMor 𝔸 𝔹) →
+  𝑓 ∘FM idFM 𝔸 ≡ 𝑓
+𝑓𝑢𝑛₀ (idFM-R 𝑓 i) A = 𝑓𝑢𝑛₀ 𝑓 A
+𝑓𝑢𝑛₁ (idFM-R 𝑓 i) t = 𝑓𝑢𝑛₁ 𝑓 t
+𝑢𝑝 (idFM-R 𝑓 i) A = idFM-R (𝑢𝑝 𝑓 A) i
+
+{-# REWRITE idFM-L idFM-R #-}
+
+record PreBSys (𝔸 : Frame ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
+  coinductive
+  field
+    𝑠ℎ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → FrameMor (𝑒𝑥 𝔸 A) 𝔸
+    𝑤𝑘 : (A : 𝑡𝑦 𝔸)→ FrameMor 𝔸 (𝑒𝑥 𝔸 A)
+    𝑧𝑣 : (A : 𝑡𝑦 𝔸) → 𝑒𝑙 (𝑒𝑥 𝔸 A) (𝑓𝑢𝑛₀ (𝑤𝑘 A) A)
+    𝑒𝑥 : (A : 𝑡𝑦 𝔸) → PreBSys (𝑒𝑥 𝔸 A)
+
+open PreBSys public
+
+record PreBMor {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄}
+               (𝑓 : FrameMor 𝔸 𝔹) (𝒜 : PreBSys 𝔸) (ℬ : PreBSys 𝔹)
+               : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+  coinductive
+  field
+    𝑠ℎ-𝑛𝑎𝑡 : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) →
+      𝑓 ∘FM 𝑠ℎ 𝒜 t ≡ 𝑠ℎ ℬ (𝑓𝑢𝑛₁ 𝑓 t) ∘FM 𝑢𝑝 𝑓 A
+    𝑤𝑘-𝑛𝑎𝑡 : (A : 𝑡𝑦 𝔸) →
+      𝑢𝑝 𝑓 A ∘FM 𝑤𝑘 𝒜 A ≡ 𝑤𝑘 ℬ (𝑓𝑢𝑛₀ 𝑓 A) ∘FM 𝑓
+    𝑧𝑣-𝑝𝑟𝑒𝑠 : (A : 𝑡𝑦 𝔸) →
+      PathP (λ i → 𝑒𝑙 (𝑒𝑥 𝔹 (𝑓𝑢𝑛₀ 𝑓 A)) (𝑓𝑢𝑛₀ (𝑤𝑘-𝑛𝑎𝑡 A i) A))
+        (𝑓𝑢𝑛₁ (𝑢𝑝 𝑓 A) (𝑧𝑣 𝒜 A)) (𝑧𝑣 ℬ (𝑓𝑢𝑛₀ 𝑓 A))
+    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → PreBMor (𝑢𝑝 𝑓 A) (𝑒𝑥 𝒜 A) (𝑒𝑥 ℬ (𝑓𝑢𝑛₀ 𝑓 A))
+
+open PreBMor public
+
+record Axioms {𝔸 : Frame ℓ₁ ℓ₂} (𝒜 : PreBSys 𝔸) : Type (ℓ₁ ⊔ ℓ₂) where
+  coinductive
+  field
+    𝑝𝒮 : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → PreBMor (𝑠ℎ 𝒜 t) (𝑒𝑥 𝒜 A) 𝒜
+    𝑝𝒲 : (A : 𝑡𝑦 𝔸) → PreBMor (𝑤𝑘 𝒜 A) 𝒜 (𝑒𝑥 𝒜 A)
+    𝑎𝑥₁ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) →
+      𝑠ℎ 𝒜 t ∘FM 𝑤𝑘 𝒜 A ≡ idFM 𝔸
+    𝑎𝑥₂ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) →
+      PathP (λ i → 𝑒𝑙 𝔸 (𝑓𝑢𝑛₀ (𝑎𝑥₁ t i) A))
+        (𝑓𝑢𝑛₁ (𝑠ℎ 𝒜 t) (𝑧𝑣 𝒜 A)) t
+    𝑎𝑥₃ : (A : 𝑡𝑦 𝔸) →
+      𝑠ℎ (𝑒𝑥 𝒜 A) (𝑧𝑣 𝒜 A) ∘FM 𝑢𝑝 (𝑤𝑘 𝒜 A) A ≡ idFM (𝑒𝑥 𝔸 A)
+    𝑒𝑥 : (A : 𝑡𝑦 𝔸) → Axioms (𝑒𝑥 𝒜 A)
+
+open Axioms public
+
+record BSys ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
+  field
+    B-𝔸 : Frame ℓ₁ ℓ₂
+    B-𝒜 : PreBSys B-𝔸
+    B-ax : Axioms B-𝒜
+
+  𝑒𝑥-B : (A : 𝑡𝑦 B-𝔸) → BSys ℓ₁ ℓ₂
+  B-𝔸 (𝑒𝑥-B A) = 𝑒𝑥 B-𝔸 A
+  B-𝒜 (𝑒𝑥-B A) = 𝑒𝑥 B-𝒜 A
+  B-ax (𝑒𝑥-B A) = 𝑒𝑥 B-ax A
+
+open BSys public
+
+record BSysMor (𝒜 : BSys ℓ₁ ℓ₂) (ℬ : BSys ℓ₃ ℓ₄)
+       : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+  field
+    B-𝑓 : FrameMor (B-𝔸 𝒜) (B-𝔸 ℬ)
+    B-p : PreBMor B-𝑓 (B-𝒜 𝒜) (B-𝒜 ℬ)
+
+  𝑢𝑝-BM : (A : 𝑡𝑦 (B-𝔸 𝒜)) → BSysMor (𝑒𝑥-B 𝒜 A) (𝑒𝑥-B ℬ (𝑓𝑢𝑛₀ B-𝑓 A))
+  B-𝑓 (𝑢𝑝-BM A) = 𝑢𝑝 B-𝑓 A
+  B-p (𝑢𝑝-BM A) = 𝑢𝑝 B-p A
+
+open BSysMor public
+
+-- PreBMor Constructions
+
+idPBM : {𝔸 : Frame ℓ₁ ℓ₂} (𝒜 : PreBSys 𝔸) → PreBMor (idFM 𝔸) 𝒜 𝒜
+𝑠ℎ-𝑛𝑎𝑡 (idPBM 𝒜) t = refl
+𝑤𝑘-𝑛𝑎𝑡 (idPBM 𝒜) A = refl
+𝑧𝑣-𝑝𝑟𝑒𝑠 (idPBM 𝒜) A = refl
+𝑢𝑝 (idPBM 𝒜) A = idPBM (𝑒𝑥 𝒜 A)
+
+𝑧𝑣Lem : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {𝑓₁ 𝑓₂ 𝑓₃ : FrameMor 𝔸 𝔹}
+  (p : 𝑓₁ ≡ 𝑓₂) (q : 𝑓₂ ≡ 𝑓₃) (A : 𝑡𝑦 𝔸) →
+  Path (𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ 𝑓₁ A) ≡ 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ 𝑓₃ A))
+    (λ i → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ((p ∙ q) i) A))
+    ((λ i → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ (p i) A)) ∙ (λ i → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ (q i) A)))
+𝑧𝑣Lem {𝔹 = 𝔹} p q A = cong-∙ (λ x → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ x A)) p q
+
+_∘PBM_ : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝒞 : PreBSys ℂ}
+  {𝑓 : FrameMor 𝔹 ℂ} {𝑔 : FrameMor 𝔸 𝔹} →
+  PreBMor 𝑓 ℬ 𝒞 → PreBMor 𝑔 𝒜 ℬ → PreBMor (𝑓 ∘FM 𝑔) 𝒜 𝒞
+𝑠ℎ-𝑛𝑎𝑡 (_∘PBM_ {𝑓 = 𝑓} {𝑔} 𝒻 ℊ) {A} t =
+  ap (𝑓 ∘FM_) (𝑠ℎ-𝑛𝑎𝑡 ℊ t) ∙ ap (_∘FM 𝑢𝑝 𝑔 A) (𝑠ℎ-𝑛𝑎𝑡 𝒻 (𝑓𝑢𝑛₁ 𝑔 t))
+𝑤𝑘-𝑛𝑎𝑡 (_∘PBM_ {𝑓 = 𝑓} {𝑔} 𝒻 ℊ) A =
+  ap (𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A) ∘FM_) (𝑤𝑘-𝑛𝑎𝑡 ℊ A) ∙ ap (_∘FM 𝑔) (𝑤𝑘-𝑛𝑎𝑡 𝒻 (𝑓𝑢𝑛₀ 𝑔 A))
+𝑧𝑣-𝑝𝑟𝑒𝑠 (_∘PBM_ {𝒜 = 𝒜} {ℬ} {𝒞} {𝑓} {𝑔} 𝒻 ℊ) A =
+  transport
+    (λ i → PathP
+      (λ j → 𝑧𝑣Lem
+        (ap (𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A) ∘FM_) (𝑤𝑘-𝑛𝑎𝑡 ℊ A))
+        (ap (_∘FM 𝑔) (𝑤𝑘-𝑛𝑎𝑡 𝒻 (𝑓𝑢𝑛₀ 𝑔 A))) A (~ i) j)
+      (𝑓𝑢𝑛₁ (𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A)) (𝑓𝑢𝑛₁ (𝑢𝑝 𝑔 A) (𝑧𝑣 𝒜 A)))
+      (𝑧𝑣 𝒞 (𝑓𝑢𝑛₀ 𝑓 (𝑓𝑢𝑛₀ 𝑔 A))))
+    (compPathP
+      (λ i → 𝑓𝑢𝑛₁ (𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A)) (𝑧𝑣-𝑝𝑟𝑒𝑠 ℊ A i))
+      (𝑧𝑣-𝑝𝑟𝑒𝑠 𝒻 (𝑓𝑢𝑛₀ 𝑔 A)))
+𝑢𝑝 (_∘PBM_ {𝑔 = 𝑔} 𝒻 ℊ) A = 𝑢𝑝 𝒻 (𝑓𝑢𝑛₀ 𝑔 A) ∘PBM 𝑢𝑝 ℊ A
+
+-- Contexts
+
+data 𝐶𝑡𝑥 (𝔸 : Frame ℓ₁ ℓ₂) : Type ℓ₁
+
+𝑒𝑥𝑠 : (𝔸 : Frame ℓ₁ ℓ₂) → 𝐶𝑡𝑥 𝔸 → Frame ℓ₁ ℓ₂
+
+data 𝐶𝑡𝑥 𝔸 where
+  ∅ : 𝐶𝑡𝑥 𝔸
+  _⊹_ : (Γ : 𝐶𝑡𝑥 𝔸) → 𝑡𝑦 (𝑒𝑥𝑠 𝔸 Γ) → 𝐶𝑡𝑥 𝔸
+
+𝑒𝑥𝑠 𝔸 ∅ = 𝔸
+𝑒𝑥𝑠 𝔸 (Γ ⊹ A) = 𝑒𝑥 (𝑒𝑥𝑠 𝔸 Γ) A
+
+𝑒𝑥𝑠-𝒜 : {𝔸 : Frame ℓ₁ ℓ₂} (𝒜 : PreBSys 𝔸) (Γ : 𝐶𝑡𝑥 𝔸) → PreBSys (𝑒𝑥𝑠 𝔸 Γ)
+𝑒𝑥𝑠-𝒜 𝒜 ∅ = 𝒜
+𝑒𝑥𝑠-𝒜 𝒜 (Γ ⊹ A) = 𝑒𝑥 (𝑒𝑥𝑠-𝒜 𝒜 Γ) A
+
+𝑒𝑥𝑠-ax : {𝔸 : Frame ℓ₁ ℓ₂} {𝒜 : PreBSys 𝔸} →
+  Axioms 𝒜 → (Γ : 𝐶𝑡𝑥 𝔸) → Axioms (𝑒𝑥𝑠-𝒜 𝒜 Γ)
+𝑒𝑥𝑠-ax ax ∅ = ax
+𝑒𝑥𝑠-ax ax (Γ ⊹ A) = 𝑒𝑥 (𝑒𝑥𝑠-ax ax Γ) A
+
+𝑒𝑥𝑠-B : (ℬ : BSys ℓ₁ ℓ₂) (Γ : 𝐶𝑡𝑥 (B-𝔸 ℬ)) → BSys ℓ₁ ℓ₂
+B-𝔸 (𝑒𝑥𝑠-B ℬ Γ) = 𝑒𝑥𝑠 (B-𝔸 ℬ) Γ
+B-𝒜 (𝑒𝑥𝑠-B ℬ Γ) = 𝑒𝑥𝑠-𝒜 (B-𝒜 ℬ) Γ
+B-ax (𝑒𝑥𝑠-B ℬ Γ) = 𝑒𝑥𝑠-ax (B-ax ℬ) Γ
+
+map𝐶𝑡𝑥 : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} →
+  FrameMor 𝔸 𝔹 → 𝐶𝑡𝑥 𝔸 → 𝐶𝑡𝑥 𝔹
+𝑢𝑝𝑠 : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄}
+  (𝑓 : FrameMor 𝔸 𝔹) (Γ : 𝐶𝑡𝑥 𝔸) → FrameMor (𝑒𝑥𝑠 𝔸 Γ) (𝑒𝑥𝑠 𝔹 (map𝐶𝑡𝑥 𝑓 Γ))
+
+map𝐶𝑡𝑥 𝑓 ∅ = ∅
+map𝐶𝑡𝑥 𝑓 (Γ ⊹ A) = map𝐶𝑡𝑥 𝑓 Γ ⊹ 𝑓𝑢𝑛₀ (𝑢𝑝𝑠 𝑓 Γ) A
+
+𝑢𝑝𝑠 𝑓 ∅ = 𝑓
+𝑢𝑝𝑠 𝑓 (Γ ⊹ A) = 𝑢𝑝 (𝑢𝑝𝑠 𝑓 Γ) A
+
+𝑢𝑝𝑠-p : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄}
+  {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝑓 : FrameMor 𝔸 𝔹} →
+  PreBMor 𝑓 𝒜 ℬ → (Γ : 𝐶𝑡𝑥 𝔸) →
+  PreBMor (𝑢𝑝𝑠 𝑓 Γ) (𝑒𝑥𝑠-𝒜 𝒜 Γ) (𝑒𝑥𝑠-𝒜 ℬ (map𝐶𝑡𝑥 𝑓 Γ))
+𝑢𝑝𝑠-p p ∅ = p
+𝑢𝑝𝑠-p p (Γ ⊹ A) = 𝑢𝑝 (𝑢𝑝𝑠-p p Γ) A
+
+map𝐶𝑡𝑥² : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  (𝑓 : FrameMor 𝔹 ℂ) (𝑔 : FrameMor 𝔸 𝔹) (Γ : 𝐶𝑡𝑥 𝔸) →
+  map𝐶𝑡𝑥 𝑓 (map𝐶𝑡𝑥 𝑔 Γ) ≡ map𝐶𝑡𝑥 (𝑓 ∘FM 𝑔) Γ
+∘𝑢𝑝𝑠 : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  (𝑓 : FrameMor 𝔹 ℂ) (𝑔 : FrameMor 𝔸 𝔹) (Γ : 𝐶𝑡𝑥 𝔸) →
+  PathP (λ i → FrameMor (𝑒𝑥𝑠 𝔸 Γ) (𝑒𝑥𝑠 ℂ (map𝐶𝑡𝑥² 𝑓 𝑔 Γ i)))
+    (𝑢𝑝𝑠 𝑓 (map𝐶𝑡𝑥 𝑔 Γ) ∘FM 𝑢𝑝𝑠 𝑔 Γ) (𝑢𝑝𝑠 (𝑓 ∘FM 𝑔) Γ) 
+
+map𝐶𝑡𝑥² 𝑓 𝑔 ∅ = refl
+map𝐶𝑡𝑥² 𝑓 𝑔 (Γ ⊹ A) i = map𝐶𝑡𝑥² 𝑓 𝑔 Γ i ⊹ 𝑓𝑢𝑛₀ (∘𝑢𝑝𝑠 𝑓 𝑔 Γ i) A
+
+∘𝑢𝑝𝑠 𝑓 𝑔 ∅ = refl
+∘𝑢𝑝𝑠 𝑓 𝑔 (Γ ⊹ A) i = 𝑢𝑝 (∘𝑢𝑝𝑠 𝑓 𝑔 Γ i) A
+
+{-# REWRITE map𝐶𝑡𝑥² #-}
+
+-- 𝐸𝑙𝑠
+
+data 𝐸𝑙𝑠 {𝔸 : Frame ℓ₁ ℓ₂} (𝒜 : PreBSys 𝔸) : 𝐶𝑡𝑥 𝔸 → Type (ℓ₁ ⊔ ℓ₂)
+
+𝑠ℎ𝑠 : {𝔸 : Frame ℓ₁ ℓ₂} {Γ : 𝐶𝑡𝑥 𝔸} (𝒜 : PreBSys 𝔸) →
+  𝐸𝑙𝑠 𝒜 Γ → FrameMor (𝑒𝑥𝑠 𝔸 Γ) 𝔸
+
+data 𝐸𝑙𝑠 {𝔸 = 𝔸} 𝒜 where
+  ! : 𝐸𝑙𝑠 𝒜 ∅
+  _⊕_ : {Γ : 𝐶𝑡𝑥 𝔸} {A : 𝑡𝑦 (𝑒𝑥𝑠 𝔸 Γ)}
+    (σ : 𝐸𝑙𝑠 𝒜 Γ) → 𝑒𝑙 𝔸 (𝑓𝑢𝑛₀ (𝑠ℎ𝑠 𝒜 σ) A) → 𝐸𝑙𝑠 𝒜 (Γ ⊹ A)
+
+𝑠ℎ𝑠 {𝔸 = 𝔸} 𝒜 ! = idFM 𝔸
+𝑠ℎ𝑠 {Γ = Γ ⊹ A} 𝒜 (σ ⊕ t) = 𝑠ℎ 𝒜 t ∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A
+
+map𝐸𝑙𝑠 : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {Γ : 𝐶𝑡𝑥 𝔸}
+  {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝑓 : FrameMor 𝔸 𝔹} →
+  PreBMor 𝑓 𝒜 ℬ → 𝐸𝑙𝑠 𝒜 Γ → 𝐸𝑙𝑠 ℬ (map𝐶𝑡𝑥 𝑓 Γ)
+𝑠ℎ𝑠-𝑛𝑎𝑡 : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {Γ : 𝐶𝑡𝑥 𝔸}
+  {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝑓 : FrameMor 𝔸 𝔹}
+  (𝒻 : PreBMor 𝑓 𝒜 ℬ) (σ : 𝐸𝑙𝑠 𝒜 Γ) →
+  𝑓 ∘FM 𝑠ℎ𝑠 𝒜 σ ≡ 𝑠ℎ𝑠 ℬ (map𝐸𝑙𝑠 𝒻 σ) ∘FM 𝑢𝑝𝑠 𝑓 Γ
+
+𝑠ℎ𝑠-p : (ℬ : BSys ℓ₁ ℓ₂) {Γ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} (σ : 𝐸𝑙𝑠 (B-𝒜 ℬ) Γ) →
+  PreBMor (𝑠ℎ𝑠 (B-𝒜 ℬ) σ) (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) (B-𝒜 ℬ)
+𝑠ℎ𝑠-p ℬ ! = idPBM (B-𝒜 ℬ)
+𝑠ℎ𝑠-p ℬ {Γ ⊹ A} (σ ⊕ t) = 𝑝𝒮 (B-ax ℬ) t ∘PBM 𝑢𝑝 (𝑠ℎ𝑠-p ℬ σ) A
+
+map𝐸𝑙𝑠 𝒻 ! = !
+map𝐸𝑙𝑠 {𝔹 = 𝔹} {Γ ⊹ A} {𝑓 = 𝑓} 𝒻 (σ ⊕ t) =
+  map𝐸𝑙𝑠 𝒻 σ ⊕ transport (λ i → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ (𝑠ℎ𝑠-𝑛𝑎𝑡 𝒻 σ i) A)) (𝑓𝑢𝑛₁ 𝑓 t)
+
+𝑠ℎ𝑠-𝑛𝑎𝑡 {𝑓 = 𝑓} 𝒻 ! = refl
+𝑠ℎ𝑠-𝑛𝑎𝑡 {𝔸 = 𝔸} {𝔹} {Γ ⊹ A} {𝒜} {ℬ} {𝑓} 𝒻 (σ ⊕ t) =
+  ap (_∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A) (𝑠ℎ-𝑛𝑎𝑡 𝒻 t)
+    ∙
+  (λ i → 𝑠ℎ ℬ (subst-filler
+    (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 𝒻 σ) (𝑓𝑢𝑛₁ 𝑓 t) i)
+    ∘FM 𝑢𝑝 (𝑠ℎ𝑠-𝑛𝑎𝑡 𝒻 σ i) A)
+
+map𝐸𝑙𝑠² : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  {Γ : 𝐶𝑡𝑥 𝔸} {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝒞 : PreBSys ℂ}
+  {𝑓 : FrameMor 𝔹 ℂ} {𝑔 : FrameMor 𝔸 𝔹}
+  (𝒻 : PreBMor 𝑓 ℬ 𝒞) (ℊ : PreBMor 𝑔 𝒜 ℬ) (σ : 𝐸𝑙𝑠 𝒜 Γ) →
+  PathP (λ i → 𝐸𝑙𝑠 𝒞 (map𝐶𝑡𝑥² 𝑓 𝑔 Γ i))
+    (map𝐸𝑙𝑠 𝒻 (map𝐸𝑙𝑠 ℊ σ)) (map𝐸𝑙𝑠 (𝒻 ∘PBM ℊ) σ)
+
+∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  {Γ : 𝐶𝑡𝑥 𝔸} {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝒞 : PreBSys ℂ}
+  {𝑓 : FrameMor 𝔹 ℂ} {𝑔 : FrameMor 𝔸 𝔹}
+  (𝒻 : PreBMor 𝑓 ℬ 𝒞) (ℊ : PreBMor 𝑔 𝒜 ℬ) (σ : 𝐸𝑙𝑠 𝒜 Γ) →
+  PathP
+    (λ i → 𝑓 ∘FM 𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ (~ i) ≡ 𝑠ℎ𝑠 𝒞 (map𝐸𝑙𝑠² 𝒻 ℊ σ i) ∘FM ∘𝑢𝑝𝑠 𝑓 𝑔 Γ i)
+    (ap (_∘FM 𝑢𝑝𝑠 𝑔 Γ) (𝑠ℎ𝑠-𝑛𝑎𝑡 𝒻 (map𝐸𝑙𝑠 ℊ σ)))
+    (𝑠ℎ𝑠-𝑛𝑎𝑡 (𝒻 ∘PBM ℊ) σ)
+
+∘𝑠ℎ𝑠-𝑛𝑎𝑡-filler : {𝔸 : Frame ℓ₁ ℓ₂} {𝔹 : Frame ℓ₃ ℓ₄} {ℂ : Frame ℓ₅ ℓ₆}
+  {Γ : 𝐶𝑡𝑥 𝔸} {𝒜 : PreBSys 𝔸} {ℬ : PreBSys 𝔹} {𝒞 : PreBSys ℂ}
+  {𝑓 : FrameMor 𝔹 ℂ} {𝑔 : FrameMor 𝔸 𝔹}
+  (𝒻 : PreBMor 𝑓 ℬ 𝒞) (ℊ : PreBMor 𝑔 𝒜 ℬ) (σ : 𝐸𝑙𝑠 𝒜 Γ)
+  {A : 𝑡𝑦 (𝑒𝑥𝑠 𝔸 Γ)} (t : 𝑒𝑙 𝔸 (𝑓𝑢𝑛₀ (𝑠ℎ𝑠 𝒜 σ) A)) (j : I) →
+  PathP (λ i → 𝑒𝑙 ℂ (𝑓𝑢𝑛₀ (∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem 𝒻 ℊ σ i j) A))
+    (subst-filler
+      (λ ℎ → 𝑒𝑙 ℂ (𝑓𝑢𝑛₀ ℎ (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 𝑔 Γ) A))) (𝑠ℎ𝑠-𝑛𝑎𝑡 𝒻 (map𝐸𝑙𝑠 ℊ σ))
+      (𝑓𝑢𝑛₁ 𝑓 (subst (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ) (𝑓𝑢𝑛₁ 𝑔 t))) j)
+    (subst-filler
+      (λ ℎ → 𝑒𝑙 ℂ (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 (𝒻 ∘PBM ℊ) σ) (𝑓𝑢𝑛₁ 𝑓 (𝑓𝑢𝑛₁ 𝑔 t)) j)
+
+map𝐸𝑙𝑠² 𝒻 ℊ ! = refl
+map𝐸𝑙𝑠² 𝒻 ℊ (σ ⊕ t) i = map𝐸𝑙𝑠² 𝒻 ℊ σ i ⊕ ∘𝑠ℎ𝑠-𝑛𝑎𝑡-filler 𝒻 ℊ σ t i1 i
+
+∘𝑠ℎ𝑠-𝑛𝑎𝑡-filler {𝔸 = 𝔸} {𝔹} {ℂ} {Γ} {𝑓 = 𝑓} {𝑔} 𝒻 ℊ σ {A} t j i =
+  subst-filler (λ ℎ → 𝑒𝑙 ℂ (𝑓𝑢𝑛₀ ℎ A)) (∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem 𝒻 ℊ σ i)
+    (𝑓𝑢𝑛₁ 𝑓 (subst-filler (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ)
+      (𝑓𝑢𝑛₁ 𝑔 t) (~ i))) j
+
+∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem 𝒻 ℊ ! j = refl
+∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem {𝔸 = 𝔸} {𝔹} {ℂ} {Γ ⊹ A} {𝒜 = 𝒜} {ℬ} {𝒞} {𝑓 = 𝑓} {𝑔} 𝒻 ℊ
+  (σ ⊕ t) =
+  cong-∙ (_∘FM 𝑢𝑝 (𝑢𝑝𝑠 𝑔 Γ) A) _ _ ◁
+    ((λ i →
+      doubleCompPath-filler
+        (ap (𝑓 ∘FM_) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ (σ ⊕ t)))
+        (λ k → 𝑠ℎ-𝑛𝑎𝑡 𝒻
+          (subst-filler (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ) (𝑓𝑢𝑛₁ 𝑔 t)
+            (~ k ∨ ~ i)) k ∘FM 𝑢𝑝 (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ (~ k ∨ ~ i)) A)
+        refl i
+      ∙ (λ k → 𝑠ℎ 𝒞 (∘𝑠ℎ𝑠-𝑛𝑎𝑡-filler 𝒻 ℊ σ t k i)
+           ∘FM 𝑢𝑝 (∘𝑠ℎ𝑠-𝑛𝑎𝑡-lem 𝒻 ℊ σ i k) A))
+    ▷ ap
+      (_∙ (λ k → 𝑠ℎ 𝒞
+        (subst-filler (λ ℎ → 𝑒𝑙 ℂ (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 (𝒻 ∘PBM ℊ) σ)
+          (𝑓𝑢𝑛₁ 𝑓 (𝑓𝑢𝑛₁ 𝑔 t)) k)
+          ∘FM 𝑢𝑝 (𝑠ℎ𝑠-𝑛𝑎𝑡 (𝒻 ∘PBM ℊ) σ k) A))
+      ((λ i →
+        compPath≡compPath'
+          (λ j → 𝑓 ∘FM
+            ((λ k → 𝑠ℎ-𝑛𝑎𝑡 ℊ t k ∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A) ∙
+             (λ k → 𝑠ℎ ℬ (subst-filler (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ)
+               (𝑓𝑢𝑛₁ 𝑔 t) (k ∧ ~ i)) ∘FM 𝑢𝑝 (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ (k ∧ ~ i)) A)) j)
+          (λ k → 𝑠ℎ-𝑛𝑎𝑡 𝒻 (subst-filler (λ ℎ → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ ℎ A)) (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ)
+            (𝑓𝑢𝑛₁ 𝑔 t) (~ k ∧ ~ i)) k ∘FM 𝑢𝑝 (𝑠ℎ𝑠-𝑛𝑎𝑡 ℊ σ (~ k ∧ ~ i)) A)
+          (~ i)) ∙
+      (λ i →
+         (λ j → 𝑓 ∘FM (rUnit (λ k → 𝑠ℎ-𝑛𝑎𝑡 ℊ t k ∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A) (~ i) j))
+         ∙ (λ j → 𝑠ℎ-𝑛𝑎𝑡 𝒻 (𝑓𝑢𝑛₁ 𝑔 t) j ∘FM
+           𝑢𝑝 𝑔 (𝑓𝑢𝑛₀ (𝑠ℎ𝑠 𝒜 σ) A) ∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A)) ∙
+      cong-∙ (_∘FM 𝑢𝑝 (𝑠ℎ𝑠 𝒜 σ) A)
+        (λ j → 𝑓 ∘FM 𝑠ℎ-𝑛𝑎𝑡 ℊ t j)
+        (λ j → 𝑠ℎ-𝑛𝑎𝑡 𝒻 (𝑓𝑢𝑛₁ 𝑔 t) j ∘FM 𝑢𝑝 𝑔 (𝑓𝑢𝑛₀ (𝑠ℎ𝑠 𝒜 σ) A)) ⁻¹))
+
+-- 𝑅𝑒𝑛
+
+data 𝑅𝑒𝑛 (ℬ : BSys ℓ₁ ℓ₂) : 𝐶𝑡𝑥 (B-𝔸 ℬ) → 𝐶𝑡𝑥 (B-𝔸 ℬ) → Type ℓ₁
+
+𝑤𝑘𝑠-𝑅𝑒𝑛 : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} →
+  𝑅𝑒𝑛 ℬ Γ Δ → FrameMor (B-𝔸 (𝑒𝑥𝑠-B ℬ Δ)) (B-𝔸 (𝑒𝑥𝑠-B ℬ Γ))
+
+data 𝑅𝑒𝑛 ℬ where
+  done : 𝑅𝑒𝑛 ℬ ∅ ∅
+  no : {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} (A : 𝑡𝑦 (B-𝔸 (𝑒𝑥𝑠-B ℬ Γ))) →
+    𝑅𝑒𝑛 ℬ Γ Δ → 𝑅𝑒𝑛 ℬ (Γ ⊹ A) Δ
+  yes : {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} (A : 𝑡𝑦 (B-𝔸 (𝑒𝑥𝑠-B ℬ Δ)))
+    (σ : 𝑅𝑒𝑛 ℬ Γ Δ) → 𝑅𝑒𝑛 ℬ (Γ ⊹ 𝑓𝑢𝑛₀ (𝑤𝑘𝑠-𝑅𝑒𝑛 σ) A) (Δ ⊹ A)
+
+𝑤𝑘𝑠-𝑅𝑒𝑛 {ℬ = ℬ} done = idFM (B-𝔸 ℬ)
+𝑤𝑘𝑠-𝑅𝑒𝑛 {ℬ = ℬ} {Γ ⊹ B} (no A σ) = 𝑤𝑘 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) B ∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 σ
+𝑤𝑘𝑠-𝑅𝑒𝑛 (yes A σ) = 𝑢𝑝 (𝑤𝑘𝑠-𝑅𝑒𝑛 σ) A
+
+𝑤𝑘𝑠-𝑅𝑒𝑛-p : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} (σ : 𝑅𝑒𝑛 ℬ Γ Δ) →
+  PreBMor (𝑤𝑘𝑠-𝑅𝑒𝑛 σ) (B-𝒜 (𝑒𝑥𝑠-B ℬ Δ)) (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ))
+𝑤𝑘𝑠-𝑅𝑒𝑛-p {ℬ = ℬ} done = idPBM (B-𝒜 ℬ)
+𝑤𝑘𝑠-𝑅𝑒𝑛-p {ℬ = ℬ} {Γ = Γ ⊹ A} (no A σ) =
+  𝑝𝒲 (B-ax (𝑒𝑥𝑠-B ℬ Γ)) A ∘PBM 𝑤𝑘𝑠-𝑅𝑒𝑛-p σ
+𝑤𝑘𝑠-𝑅𝑒𝑛-p (yes A σ) = 𝑢𝑝 (𝑤𝑘𝑠-𝑅𝑒𝑛-p σ) A
+
+subst-ap : {A : Type ℓ₁} {B : A → Type ℓ₂} {C : A → Type ℓ₃}
+  (f : {x : A} → B x → C x) {x y : A} (p : x ≡ y) (α : B x) (φ : I) →
+  f (subst-filler B p α φ) ≡ subst-filler C p (f α) φ
+
+comp𝑅𝑒𝑛 : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ Σ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} →
+  𝑅𝑒𝑛 ℬ Γ Δ → 𝑅𝑒𝑛 ℬ Δ Σ → 𝑅𝑒𝑛 ℬ Γ Σ
+comp-𝑤𝑘𝑠-𝑅𝑒𝑛 : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ Σ : 𝐶𝑡𝑥 (B-𝔸 ℬ)}
+  (σ : 𝑅𝑒𝑛 ℬ Γ Δ) (τ : 𝑅𝑒𝑛 ℬ Δ Σ) →
+  𝑤𝑘𝑠-𝑅𝑒𝑛 σ ∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 τ ≡ 𝑤𝑘𝑠-𝑅𝑒𝑛 (comp𝑅𝑒𝑛 σ τ)
+
+comp𝑅𝑒𝑛 done done = done
+comp𝑅𝑒𝑛 (no A σ) τ = no A (comp𝑅𝑒𝑛 σ τ)
+comp𝑅𝑒𝑛 (yes A σ) (no _ τ) = no (𝑓𝑢𝑛₀ (𝑤𝑘𝑠-𝑅𝑒𝑛 σ) A) (comp𝑅𝑒𝑛 σ τ)
+comp𝑅𝑒𝑛 {ℬ = ℬ} {Γ ⊹ _} {Δ ⊹ _} {Σ = Σ ⊹ A} (yes _ σ) (yes A τ) =
+  subst (λ ℎ → 𝑅𝑒𝑛 ℬ (Γ ⊹ 𝑓𝑢𝑛₀ ℎ A) (Σ ⊹ A))
+    (comp-𝑤𝑘𝑠-𝑅𝑒𝑛 σ τ ⁻¹) (yes A (comp𝑅𝑒𝑛 σ τ))
+
+comp-𝑤𝑘𝑠-𝑅𝑒𝑛 done done = refl
+comp-𝑤𝑘𝑠-𝑅𝑒𝑛 {ℬ = ℬ} {Γ ⊹ _} (no A σ) τ =
+  ap (𝑤𝑘 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) A ∘FM_) (comp-𝑤𝑘𝑠-𝑅𝑒𝑛 σ τ)
+comp-𝑤𝑘𝑠-𝑅𝑒𝑛 {ℬ = ℬ} {Γ ⊹ _} (yes A σ) (no _ τ) =
+  ap (_∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 τ) (𝑤𝑘-𝑛𝑎𝑡 (𝑤𝑘𝑠-𝑅𝑒𝑛-p σ) A) ∙
+  ap (𝑤𝑘 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) _ ∘FM_) (comp-𝑤𝑘𝑠-𝑅𝑒𝑛 σ τ)
+comp-𝑤𝑘𝑠-𝑅𝑒𝑛 {ℬ = ℬ} {Γ ⊹ _} {Δ ⊹ _} {Σ ⊹ _} (yes _ σ) (yes A τ) =
+  fromPathP (λ i → 𝑢𝑝 (comp-𝑤𝑘𝑠-𝑅𝑒𝑛 σ τ (~ i)) A) ⁻¹ ∙
+  subst-ap
+    {B = λ ℎ → 𝑅𝑒𝑛 ℬ (Γ ⊹ 𝑓𝑢𝑛₀ ℎ A) (Σ ⊹ A)}
+    𝑤𝑘𝑠-𝑅𝑒𝑛
+    (comp-𝑤𝑘𝑠-𝑅𝑒𝑛 σ τ ⁻¹)
+    (yes A (comp𝑅𝑒𝑛 σ τ)) i1 ⁻¹
+
+map𝑅𝑒𝑛 : {ℬ : BSys ℓ₁ ℓ₂} {𝒞 : BSys ℓ₃ ℓ₄} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} 
+  (𝒻 : BSysMor ℬ 𝒞) → 𝑅𝑒𝑛 ℬ Γ Δ →
+  𝑅𝑒𝑛 𝒞 (map𝐶𝑡𝑥 (B-𝑓 𝒻) Γ) (map𝐶𝑡𝑥 (B-𝑓 𝒻) Δ)
+𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 : {ℬ : BSys ℓ₁ ℓ₂} {𝒞 : BSys ℓ₃ ℓ₄} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} → 
+  (𝒻 : BSysMor ℬ 𝒞) (σ : 𝑅𝑒𝑛 ℬ Γ Δ) →
+  𝑢𝑝𝑠 (B-𝑓 𝒻) Γ ∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 σ ≡ 𝑤𝑘𝑠-𝑅𝑒𝑛 (map𝑅𝑒𝑛 𝒻 σ) ∘FM 𝑢𝑝𝑠 (B-𝑓 𝒻) Δ
+
+map𝑅𝑒𝑛 𝒻 done = done
+map𝑅𝑒𝑛 {Γ = Γ ⊹ A} 𝒻 (no A σ) = no (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (B-𝑓 𝒻) Γ) A) (map𝑅𝑒𝑛 𝒻 σ)
+map𝑅𝑒𝑛 {𝒞 = 𝒞} {Γ = Γ ⊹ _} {Δ ⊹ A} 𝒻 (yes A σ) =
+  subst (λ ℎ → 𝑅𝑒𝑛 𝒞 (map𝐶𝑡𝑥 (B-𝑓 𝒻) Γ ⊹ 𝑓𝑢𝑛₀ ℎ A) (map𝐶𝑡𝑥 (B-𝑓 𝒻) (Δ ⊹ A)))
+    (𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 σ ⁻¹) (yes (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A) (map𝑅𝑒𝑛 𝒻 σ))
+
+𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 done = refl
+𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 {𝒞 = 𝒞} {Γ = Γ ⊹ A} 𝒻 (no A σ) =
+  ap (_∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 σ) (𝑤𝑘-𝑛𝑎𝑡 (𝑢𝑝𝑠-p (B-p 𝒻) Γ) A)
+    ∙ ap (𝑤𝑘 (B-𝒜 (𝑒𝑥𝑠-B 𝒞 (map𝐶𝑡𝑥 (B-𝑓 𝒻) Γ))) _ ∘FM_) (𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 σ)
+𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 {ℬ = ℬ} {𝒞} {Γ ⊹ _} {Δ ⊹ _} 𝒻 (yes A σ) =
+  fromPathP (ap (λ ℎ → 𝑢𝑝 ℎ A) (𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 σ ⁻¹)) ⁻¹ ∙
+  subst-ap
+    {B = λ ℎ →
+         FrameMor
+         (𝑒𝑥𝑠 (B-𝔸 𝒞) (map𝐶𝑡𝑥 (B-𝑓 𝒻) (Δ ⊹ A)))
+         (𝑒𝑥𝑠 (B-𝔸 𝒞) (map𝐶𝑡𝑥 (B-𝑓 𝒻) Γ ⊹ 𝑓𝑢𝑛₀ ℎ A))}
+    (_∘FM 𝑢𝑝 (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A)
+    (𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 σ ⁻¹)
+    (𝑢𝑝 (𝑤𝑘𝑠-𝑅𝑒𝑛 (map𝑅𝑒𝑛 𝒻 σ)) (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A))
+    i1 ⁻¹ ∙
+  (λ i →
+    subst-ap
+      {B = λ ℎ → 𝑅𝑒𝑛 𝒞 (map𝐶𝑡𝑥 (B-𝑓 𝒻) Γ ⊹ 𝑓𝑢𝑛₀ ℎ A)
+        (map𝐶𝑡𝑥 (B-𝑓 𝒻) Δ ⊹ 𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A)}
+      𝑤𝑘𝑠-𝑅𝑒𝑛
+      (𝑤𝑘𝑠-𝑅𝑒𝑛-𝑛𝑎𝑡 𝒻 σ ⁻¹)
+      (yes (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A) (map𝑅𝑒𝑛 𝒻 σ))
+      i1 (~ i) ∘FM 𝑢𝑝 (𝑢𝑝𝑠 (B-𝑓 𝒻) Δ) A)
+
+all-no : (ℬ : BSys ℓ₁ ℓ₂) (Γ : 𝐶𝑡𝑥 (B-𝔸 ℬ)) → 𝑅𝑒𝑛 ℬ Γ ∅
+all-no ℬ ∅ = done
+all-no ℬ (Γ ⊹ A) = no A (all-no ℬ Γ)
+
+𝑤𝑘𝑠 : (ℬ : BSys ℓ₁ ℓ₂) (Γ : 𝐶𝑡𝑥 (B-𝔸 ℬ)) →
+  FrameMor (B-𝔸 ℬ) (B-𝔸 (𝑒𝑥𝑠-B ℬ Γ))
+𝑤𝑘𝑠 𝒜 Γ = 𝑤𝑘𝑠-𝑅𝑒𝑛 (all-no 𝒜 Γ)
+
+𝑤𝑘𝑠-p : (ℬ : BSys ℓ₁ ℓ₂) (Γ : 𝐶𝑡𝑥 (B-𝔸 ℬ)) →
+  PreBMor (𝑤𝑘𝑠 ℬ Γ) (B-𝒜 ℬ) (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ))
+𝑤𝑘𝑠-p ℬ Γ = 𝑤𝑘𝑠-𝑅𝑒𝑛-p (all-no ℬ Γ)
+
+-- Compositional Structure
+
+data 𝑇𝑚𝑠 (ℬ : BSys ℓ₁ ℓ₂) (Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)) : Type (ℓ₁ ⊔ ℓ₂) where
+  tms : 𝐸𝑙𝑠 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) (map𝐶𝑡𝑥 (𝑤𝑘𝑠 ℬ Γ) Δ) → 𝑇𝑚𝑠 ℬ Γ Δ
+
+open 𝑇𝑚𝑠
+
+𝑠𝑢𝑏 : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} →
+  𝑇𝑚𝑠 ℬ Γ Δ → FrameMor (B-𝔸 (𝑒𝑥𝑠-B ℬ Δ)) (B-𝔸 (𝑒𝑥𝑠-B ℬ Γ))
+𝑠𝑢𝑏 {ℬ = ℬ} {Γ} {Δ} (tms σ) =
+  𝑠ℎ𝑠 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) σ ∘FM 𝑢𝑝𝑠 (𝑤𝑘𝑠 ℬ Γ) Δ
+
+𝑠𝑢𝑏-p : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} (σ : 𝑇𝑚𝑠 ℬ Γ Δ) →
+  PreBMor (𝑠𝑢𝑏 σ) (B-𝒜 (𝑒𝑥𝑠-B ℬ Δ)) (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ))
+𝑠𝑢𝑏-p {ℬ = ℬ} {Γ} {Δ} (tms σ) = 𝑠ℎ𝑠-p (𝑒𝑥𝑠-B ℬ Γ) σ ∘PBM 𝑢𝑝𝑠-p (𝑤𝑘𝑠-p ℬ Γ) Δ
+
+𝑠𝑢𝑏Lem : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ : 𝐶𝑡𝑥 (B-𝔸 ℬ)}
+  (σ : 𝐸𝑙𝑠 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) (map𝐶𝑡𝑥 (𝑤𝑘𝑠 ℬ Γ) Δ)) →
+  𝑠ℎ𝑠 (B-𝒜 (𝑒𝑥𝑠-B ℬ Γ)) σ ∘FM (𝑢𝑝𝑠 (𝑤𝑘𝑠 ℬ Γ) Δ ∘FM 𝑤𝑘𝑠-𝑅𝑒𝑛 (all-no ℬ Δ))
+    ≡ 𝑤𝑘𝑠 ℬ Γ
+𝑠𝑢𝑏Lem {ℬ = ℬ} {Γ} {∅} ! = refl
+𝑠𝑢𝑏Lem {ℬ = ℬ} {Γ} {Δ ⊹ A} (σ ⊕ t) =
+  ap (λ ℎ → 𝑠ℎ𝑠 (𝑒𝑥𝑠-𝒜 (B-𝒜 ℬ) Γ) (σ ⊕ t) ∘FM ℎ ∘FM 𝑤𝑘𝑠 ℬ Δ)
+    (𝑤𝑘-𝑛𝑎𝑡 (𝑢𝑝𝑠-p (𝑤𝑘𝑠-p ℬ Γ) Δ) A) ∙
+  ap (λ ℎ → 𝑠ℎ (𝑒𝑥𝑠-𝒜 (B-𝒜 ℬ) Γ) t ∘FM ℎ ∘FM 𝑢𝑝𝑠 (𝑤𝑘𝑠 ℬ Γ) Δ ∘FM 𝑤𝑘𝑠 ℬ Δ)
+    (𝑤𝑘-𝑛𝑎𝑡 (𝑠ℎ𝑠-p (𝑒𝑥𝑠-B ℬ Γ) σ) (𝑓𝑢𝑛₀ (𝑢𝑝𝑠 (𝑤𝑘𝑠 ℬ Γ) Δ) A)) ∙
+  ap (_∘FM (𝑠𝑢𝑏 (tms {ℬ = ℬ} {Γ} {Δ} σ) ∘FM 𝑤𝑘𝑠 ℬ Δ))
+    (𝑎𝑥₁ (B-ax (𝑒𝑥𝑠-B ℬ Γ)) t) ∙
+  𝑠𝑢𝑏Lem {Γ = Γ} {Δ} σ
+
+{-# REWRITE 𝑠𝑢𝑏Lem #-}
+
+_∘𝑇𝑚𝑠_ : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ Σ : 𝐶𝑡𝑥 (B-𝔸 ℬ)} →
+  𝑇𝑚𝑠 ℬ Δ Σ → 𝑇𝑚𝑠 ℬ Γ Δ → 𝑇𝑚𝑠 ℬ Γ Σ
+_∘𝑇𝑚𝑠_ {ℬ = ℬ} {Γ} {Δ} {Σ} (tms σ) (tms τ) =
+  tms (map𝐸𝑙𝑠 (𝑠𝑢𝑏-p {ℬ = ℬ} {Γ} {Δ} (tms τ)) σ)
+
+∘𝑇𝑚𝑠² : {ℬ : BSys ℓ₁ ℓ₂} {Γ Δ Σ Ω : 𝐶𝑡𝑥 (B-𝔸 ℬ)}
+  (σ : 𝑇𝑚𝑠 ℬ Σ Ω) (τ : 𝑇𝑚𝑠 ℬ Δ Σ) (μ : 𝑇𝑚𝑠 ℬ Γ Δ) →
+  (σ ∘𝑇𝑚𝑠 τ) ∘𝑇𝑚𝑠 μ ≡ σ ∘𝑇𝑚𝑠 (τ ∘𝑇𝑚𝑠 μ)
+∘𝑇𝑚𝑠² {ℬ = ℬ} {Γ} {Δ} {Σ} (tms σ) (tms τ) (tms μ) i =
+  {!map𝐸𝑙𝑠²
+    (𝑠ℎ𝑠-p (𝑒𝑥𝑠-B ℬ Γ) μ ∘PBM 𝑢𝑝𝑠-p (𝑤𝑘𝑠-p ℬ Γ) Δ)
+    (𝑠ℎ𝑠-p (𝑒𝑥𝑠-B ℬ Δ) τ ∘PBM 𝑢𝑝𝑠-p (𝑤𝑘𝑠-p ℬ Δ) Σ)
+    σ!}
No results found