B-Systems

bsys.agda

{-# OPTIONS --cubical --guardedness #-}

module bsys 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

-- Definition of a B-system

variable
  ℓ ℓ₁ ℓ₂ : Level

record Frame ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
  coinductive
  field
    𝑡𝑦 : Type ℓ₁
    𝑒𝑙 : 𝑡𝑦 → Type ℓ₂
    𝑢𝑝 : 𝑡𝑦 → Frame ℓ₁ ℓ₂

open Frame

record Frame-Mor (𝔸 𝔹 : Frame ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑓𝑢𝑛₀ : 𝑡𝑦 𝔸 → 𝑡𝑦 𝔹
    𝑓𝑢𝑛₁ : {A : 𝑡𝑦 𝔸} → 𝑒𝑙 𝔸 A → 𝑒𝑙 𝔹 (𝑓𝑢𝑛₀ A)
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → Frame-Mor (𝑢𝑝 𝔸 A) (𝑢𝑝 𝔹 (𝑓𝑢𝑛₀ A))

open Frame-Mor

_∘FM_ : {𝔸 𝔹 ℂ : Frame ℓ₁ ℓ₂} → Frame-Mor 𝔹 ℂ → Frame-Mor 𝔸 𝔹 → Frame-Mor 𝔸 ℂ
𝑓𝑢𝑛₀ (𝑓 ∘FM 𝑔) = 𝑓𝑢𝑛₀ 𝑓 ∘ 𝑓𝑢𝑛₀ 𝑔
𝑓𝑢𝑛₁ (𝑓 ∘FM 𝑔) = 𝑓𝑢𝑛₁ 𝑓 ∘ 𝑓𝑢𝑛₁ 𝑔
𝑢𝑝 (𝑓 ∘FM 𝑔) A = 𝑢𝑝 𝑓 (𝑓𝑢𝑛₀ 𝑔 A) ∘FM 𝑢𝑝 𝑔 A

idFM : (𝔸 : Frame ℓ₁ ℓ₂) → Frame-Mor 𝔸 𝔸
𝑓𝑢𝑛₀ (idFM 𝔸) A = A
𝑓𝑢𝑛₁ (idFM 𝔸) t = t
𝑢𝑝 (idFM 𝔸) A = idFM (𝑢𝑝 𝔸 A)

record SubStr (𝔸 : Frame ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑠ℎ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → Frame-Mor (𝑢𝑝 𝔸 A) 𝔸
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → SubStr (𝑢𝑝 𝔸 A)

open SubStr

record WkStr (𝔸 : Frame ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑤𝑘 : (A : 𝑡𝑦 𝔸)→ Frame-Mor 𝔸 (𝑢𝑝 𝔸 A)
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → WkStr (𝑢𝑝 𝔸 A)

open WkStr

record 𝑧𝑣Str {𝔸 : Frame ℓ₁ ℓ₂} (𝒲 : WkStr 𝔸) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑧𝑣 : (A : 𝑡𝑦 𝔸) → 𝑒𝑙 (𝑢𝑝 𝔸 A) (𝑓𝑢𝑛₀ (𝑤𝑘 𝒲 A) A)
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → 𝑧𝑣Str (𝑢𝑝 𝒲 A)

open 𝑧𝑣Str

record Preserves-Sub {𝔸 𝔹 : Frame ℓ₁ ℓ₂} (𝑓 : Frame-Mor 𝔸 𝔹) (𝒮₁ : SubStr 𝔸) (𝒮₂ : SubStr 𝔹)
                     : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑛𝑎𝑡 : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → 𝑓 ∘FM 𝑠ℎ 𝒮₁ t ≡ 𝑠ℎ 𝒮₂ (𝑓𝑢𝑛₁ 𝑓 t) ∘FM 𝑢𝑝 𝑓 A
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → Preserves-Sub (𝑢𝑝 𝑓 A) (𝑢𝑝 𝒮₁ A) (𝑢𝑝 𝒮₂ (𝑓𝑢𝑛₀ 𝑓 A))

open Preserves-Sub

record Preserves-Wk {𝔸 𝔹 : Frame ℓ₁ ℓ₂} (𝑓 : Frame-Mor 𝔸 𝔹) (𝒲₁ : WkStr 𝔸) (𝒲₂ : WkStr 𝔹)
                    : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑛𝑎𝑡 : (A : 𝑡𝑦 𝔸) → 𝑢𝑝 𝑓 A ∘FM 𝑤𝑘 𝒲₁ A ≡ 𝑤𝑘 𝒲₂ (𝑓𝑢𝑛₀ 𝑓 A) ∘FM 𝑓
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → Preserves-Wk (𝑢𝑝 𝑓 A) (𝑢𝑝 𝒲₁ A) (𝑢𝑝 𝒲₂ (𝑓𝑢𝑛₀ 𝑓 A))

open Preserves-Wk

record Preserves-𝑧𝑣 {𝔸 𝔹 : Frame ℓ₁ ℓ₂} {𝑓 : Frame-Mor 𝔸 𝔹} {𝒲₁ : WkStr 𝔸} {𝒲₂ : WkStr 𝔹}
                    (p : Preserves-Wk 𝑓 𝒲₁ 𝒲₂) (𝒱₁ : 𝑧𝑣Str 𝒲₁) (𝒱₂ : 𝑧𝑣Str 𝒲₂)
                    : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑝𝑟𝑒𝑠 : (A : 𝑡𝑦 𝔸) →
      PathP (λ i → 𝑒𝑙 (𝑢𝑝 𝔹 (𝑓𝑢𝑛₀ 𝑓 A)) (𝑓𝑢𝑛₀ (𝑛𝑎𝑡 p A i) A))
        (𝑓𝑢𝑛₁ (𝑢𝑝 𝑓 A) (𝑧𝑣 𝒱₁ A)) (𝑧𝑣 𝒱₂ (𝑓𝑢𝑛₀ 𝑓 A))
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → Preserves-𝑧𝑣 (𝑢𝑝 p A) (𝑢𝑝 𝒱₁ A) (𝑢𝑝 𝒱₂ (𝑓𝑢𝑛₀ 𝑓 A))

open Preserves-𝑧𝑣

record Pre-B-System (𝔸 : Frame ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  field
    B-𝒮 : SubStr 𝔸
    B-𝒲 : WkStr 𝔸
    B-𝒱 : 𝑧𝑣Str B-𝒲

  𝑢𝑝-PB : (A : 𝑡𝑦 𝔸) → Pre-B-System (𝑢𝑝 𝔸 A)
  B-𝒮 (𝑢𝑝-PB A) = 𝑢𝑝 B-𝒮 A
  B-𝒲 (𝑢𝑝-PB A) = 𝑢𝑝 B-𝒲 A
  B-𝒱 (𝑢𝑝-PB A) = 𝑢𝑝 B-𝒱 A

open Pre-B-System

record Pre-B-Mor {𝔸 𝔹 : Frame ℓ₁ ℓ₂} (𝑓 : Frame-Mor 𝔸 𝔹)
                 (𝒜 : Pre-B-System 𝔸) (ℬ : Pre-B-System 𝔹) : Type (ℓ₁ ⊔ ℓ₂) where
  field
    𝑝𝒮 : Preserves-Sub 𝑓 (B-𝒮 𝒜) (B-𝒮 ℬ)
    𝑝𝒲 : Preserves-Wk 𝑓 (B-𝒲 𝒜) (B-𝒲 ℬ)
    𝑝𝒱 :  Preserves-𝑧𝑣 𝑝𝒲 (B-𝒱 𝒜) (B-𝒱 ℬ)

  𝑢𝑝-PBM : (A : 𝑡𝑦 𝔸) → Pre-B-Mor (𝑢𝑝 𝑓 A) (𝑢𝑝-PB 𝒜 A) (𝑢𝑝-PB ℬ (𝑓𝑢𝑛₀ 𝑓 A))
  𝑝𝒮 (𝑢𝑝-PBM A) = 𝑢𝑝 𝑝𝒮 A
  𝑝𝒲 (𝑢𝑝-PBM A) = 𝑢𝑝 𝑝𝒲 A
  𝑝𝒱 (𝑢𝑝-PBM A) = 𝑢𝑝 𝑝𝒱 A

open Pre-B-Mor

record Axioms {𝔸 : Frame ℓ₁ ℓ₂} (𝒜 : Pre-B-System 𝔸) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑝𝒮 : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → Pre-B-Mor (𝑠ℎ (B-𝒮 𝒜) t) (𝑢𝑝-PB 𝒜 A) 𝒜
    𝑝𝒲 : (A : 𝑡𝑦 𝔸) → Pre-B-Mor (𝑤𝑘 (B-𝒲 𝒜) A) 𝒜 (𝑢𝑝-PB 𝒜 A)
    𝑎𝑥₁ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) → 𝑠ℎ (B-𝒮 𝒜) t ∘FM 𝑤𝑘 (B-𝒲 𝒜) A ≡ idFM 𝔸
    𝑎𝑥₂ : {A : 𝑡𝑦 𝔸} (t : 𝑒𝑙 𝔸 A) →
      PathP (λ i → 𝑒𝑙 𝔸 (𝑓𝑢𝑛₀ (𝑎𝑥₁ t i) A))
        (𝑓𝑢𝑛₁ (𝑠ℎ (B-𝒮 𝒜) t) (𝑧𝑣 (B-𝒱 𝒜) A)) t
    𝑎𝑥₃ : (A : 𝑡𝑦 𝔸) → 𝑠ℎ (𝑢𝑝 (B-𝒮 𝒜) A) (𝑧𝑣 (B-𝒱 𝒜) A) ∘FM 𝑢𝑝 (𝑤𝑘 (B-𝒲 𝒜) A) A ≡ idFM (𝑢𝑝 𝔸 A)
    𝑢𝑝 : (A : 𝑡𝑦 𝔸) → Axioms (𝑢𝑝-PB 𝒜 A)

open Axioms

record B-System ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
  field
    B-𝔸 : Frame ℓ₁ ℓ₂
    B-𝒜 : Pre-B-System B-𝔸
    B-ax : Axioms B-𝒜

  𝑢𝑝-B : (A : 𝑡𝑦 B-𝔸) → B-System ℓ₁ ℓ₂
  B-𝔸 (𝑢𝑝-B A) = 𝑢𝑝 B-𝔸 A
  B-𝒜 (𝑢𝑝-B A) = 𝑢𝑝-PB B-𝒜 A
  B-ax (𝑢𝑝-B A) = 𝑢𝑝 B-ax A

open B-System

record B-System-Mor (𝒜 ℬ : B-System ℓ₁ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  field
    B-𝑓 : Frame-Mor (B-𝔸 𝒜) (B-𝔸 ℬ)
    B-p : Pre-B-Mor B-𝑓 (B-𝒜 𝒜) (B-𝒜 ℬ)

  𝑢𝑝-BM : (A : 𝑡𝑦 (B-𝔸 𝒜)) → B-System-Mor (𝑢𝑝-B 𝒜 A) (𝑢𝑝-B ℬ (𝑓𝑢𝑛₀ B-𝑓 A))
  B-𝑓 (𝑢𝑝-BM A) = 𝑢𝑝 B-𝑓 A
  B-p (𝑢𝑝-BM A) = 𝑢𝑝-PBM B-p A

open B-System-Mor

B-𝑠ℎ : (𝒜 : B-System ℓ₁ ℓ₂) {A : 𝑡𝑦 (B-𝔸 𝒜)} (t : 𝑒𝑙 (B-𝔸 𝒜) A) → B-System-Mor (𝑢𝑝-B 𝒜 A) 𝒜
B-𝑓 (B-𝑠ℎ 𝒜 t) = 𝑠ℎ (B-𝒮 (B-𝒜 𝒜)) t
B-p (B-𝑠ℎ 𝒜 t) = 𝑝𝒮 (B-ax 𝒜) t

B-𝑤𝑘 : (𝒜 : B-System ℓ₁ ℓ₂) (A : 𝑡𝑦 (B-𝔸 𝒜)) → B-System-Mor 𝒜 (𝑢𝑝-B 𝒜 A)
B-𝑓 (B-𝑤𝑘 𝒜 A) = 𝑤𝑘 (B-𝒲 (B-𝒜 𝒜)) A
B-p (B-𝑤𝑘 𝒜 A) = 𝑝𝒲 (B-ax 𝒜) A

B-𝑧𝑣 : (𝒜 : B-System ℓ₁ ℓ₂) (A : 𝑡𝑦 (B-𝔸 𝒜)) → 𝑒𝑙 (𝑢𝑝 (B-𝔸 𝒜) A) (𝑓𝑢𝑛₀ (𝑤𝑘 (B-𝒲 (B-𝒜 𝒜)) A) A)
B-𝑧𝑣 𝒜 A = 𝑧𝑣 (B-𝒱 (B-𝒜 𝒜)) A