FrozenWinters/B.agda

## B.agda
{-# 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 ℬ Δ) Σ)
    σ!}