Dependent Multicategories (WIP)

dep.agda

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

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

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

record TyStr ℓ : Type (lsuc ℓ) where
  coinductive
  field
    𝑡𝑦 : Type ℓ
    𝑒𝑥 : 𝑡𝑦 → TyStr ℓ

open TyStr public

data 𝐶𝑡𝑥 (𝒯 : TyStr ℓ) : Type ℓ

𝑒𝑥𝑠 : (𝒯 : TyStr ℓ) → 𝐶𝑡𝑥 𝒯 → TyStr ℓ

infixl 20 _⊹_
data 𝐶𝑡𝑥 𝒯 where
  ∅ : 𝐶𝑡𝑥 𝒯
  _⊹_ : (Γ : 𝐶𝑡𝑥 𝒯) → 𝑡𝑦 (𝑒𝑥𝑠 𝒯 Γ) → 𝐶𝑡𝑥 𝒯

𝑒𝑥𝑠 𝒯 ∅ = 𝒯
𝑒𝑥𝑠 𝒯 (Γ ⊹ A) = 𝑒𝑥 (𝑒𝑥𝑠 𝒯 Γ) A

record TyMor (𝒯 : TyStr ℓ₁) (𝒮 : TyStr ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑓𝑢𝑛 : 𝑡𝑦 𝒯 → 𝑡𝑦 𝒮
    𝑢𝑝 : (A : 𝑡𝑦 𝒯) → TyMor (𝑒𝑥 𝒯 A) (𝑒𝑥 𝒮 (𝑓𝑢𝑛 A))

open TyMor

infixl 20 _∘TyMor_
_∘TyMor_ : {𝒯 : TyStr ℓ₁} {𝒮 : TyStr ℓ₂} {ℒ : TyStr ℓ₃} →
  TyMor 𝒮 ℒ → TyMor 𝒯 𝒮 → TyMor 𝒯 ℒ
𝑓𝑢𝑛 (F ∘TyMor G) = 𝑓𝑢𝑛 F ∘ 𝑓𝑢𝑛 G
𝑢𝑝 (F ∘TyMor G) A = 𝑢𝑝 F (𝑓𝑢𝑛 G A) ∘TyMor 𝑢𝑝 G A

idTyMor : (𝒯 : TyStr ℓ) → TyMor 𝒯 𝒯
𝑓𝑢𝑛 (idTyMor 𝒯) A = A
𝑢𝑝 (idTyMor 𝒯) A = idTyMor (𝑒𝑥 𝒯 A)

record ElStr (𝒯 : TyStr ℓ₁) ℓ₂ : Type (ℓ₁ ⊔ (lsuc ℓ₂)) where
  field
    𝑒𝑙 : 𝑡𝑦 𝒯 → Type ℓ₂
    𝑠ℎ : {A : 𝑡𝑦 𝒯} → 𝑒𝑙 A → TyMor (𝑒𝑥 𝒯 A) 𝒯

open ElStr

data 𝐸𝑙𝑠 {𝒯₁ : TyStr ℓ₁} {𝒯₂ : TyStr ℓ₂} (𝑓 : TyMor 𝒯₁ 𝒯₂) (ℰ : ElStr 𝒯₂ ℓ₃) : 𝐶𝑡𝑥 𝒯₁ → Type (ℓ₁ ⊔ ℓ₃)

𝑠ℎ𝑠 : {𝒯₁ : TyStr ℓ₁} {𝒯₂ : TyStr ℓ₂} (𝑓 : TyMor 𝒯₁ 𝒯₂) (ℰ : ElStr 𝒯₂ ℓ₃) {Γ : 𝐶𝑡𝑥 𝒯₁} → 𝐸𝑙𝑠 𝑓 ℰ Γ → TyMor (𝑒𝑥𝑠 𝒯₁ Γ) 𝒯₂

infixl 20 _⊕_
data 𝐸𝑙𝑠 {𝒯₁ = 𝒯₁} {𝒯₂} 𝑓 ℰ where
  ! : 𝐸𝑙𝑠 𝑓 ℰ ∅
  _⊕_ : {Γ : 𝐶𝑡𝑥 𝒯₁} {A : 𝑡𝑦 (𝑒𝑥𝑠 𝒯₁ Γ)} (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ Γ) → 𝑒𝑙 ℰ (𝑓𝑢𝑛 (𝑠ℎ𝑠 𝑓 ℰ 𝓈s) A) → 𝐸𝑙𝑠 𝑓 ℰ (Γ ⊹ A)

𝑠ℎ𝑠 𝑓 ℰ ! = 𝑓
𝑠ℎ𝑠 𝑓 ℰ {Γ ⊹ A} (𝓈s ⊕ 𝓈) = 𝑠ℎ ℰ 𝓈 ∘TyMor 𝑢𝑝 (𝑠ℎ𝑠 𝑓 ℰ 𝓈s) A

record ElMor {𝒯 𝒯₁ 𝒯₂ : TyStr ℓ₁} (𝑓 : TyMor 𝒯 𝒯₁) (𝑔 : TyMor 𝒯 𝒯₂)
              (ℰ₁ : ElStr 𝒯₁ ℓ₂) (ℰ₂ : ElStr 𝒯₂ ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    𝑓𝑢𝑛₁ : {A : 𝑡𝑦 𝒯} → 𝑒𝑙 ℰ₁ (𝑓𝑢𝑛 𝑓 A) → 𝑒𝑙 ℰ₂ (𝑓𝑢𝑛 𝑔 A)
    𝑢𝑝₁ : {A : 𝑡𝑦 𝒯} (t : 𝑒𝑙 ℰ₁ (𝑓𝑢𝑛 𝑓 A)) → ElMor (𝑠ℎ ℰ₁ t ∘TyMor 𝑢𝑝 𝑓 A) (𝑠ℎ ℰ₂ (𝑓𝑢𝑛₁ t) ∘TyMor 𝑢𝑝 𝑔 A) ℰ₁ ℰ₂

open ElMor

idElMor : {𝒯₁ 𝒯₂ : TyStr ℓ₁} (𝑓 : TyMor 𝒯₁ 𝒯₂) (ℰ : ElStr 𝒯₂ ℓ₂) → ElMor 𝑓 𝑓 ℰ ℰ
𝑓𝑢𝑛₁ (idElMor 𝑓 ℰ) t = t
𝑢𝑝₁ (idElMor 𝑓 ℰ) {A} t = idElMor (𝑠ℎ ℰ t ∘TyMor 𝑢𝑝 𝑓 A) ℰ

_∘ElMor_ : {𝒯 𝒯₁ 𝒯₂ 𝒯₃ : TyStr ℓ₁} {𝑓 : TyMor 𝒯 𝒯₁} {𝑔 : TyMor 𝒯 𝒯₂} {ℎ : TyMor 𝒯 𝒯₃}
  {ℰ₁ : ElStr 𝒯₁ ℓ₂} {ℰ₂ : ElStr 𝒯₂ ℓ₂} {ℰ₃ : ElStr 𝒯₃ ℓ₂} →
  ElMor 𝑔 ℎ ℰ₂ ℰ₃ → ElMor 𝑓 𝑔 ℰ₁ ℰ₂ → ElMor 𝑓 ℎ ℰ₁ ℰ₃
𝑓𝑢𝑛₁ (𝒻 ∘ElMor ℊ) = 𝑓𝑢𝑛₁ 𝒻 ∘ 𝑓𝑢𝑛₁ ℊ
𝑢𝑝₁ (𝒻 ∘ElMor ℊ) t = 𝑢𝑝₁ 𝒻 (𝑓𝑢𝑛₁ ℊ t) ∘ElMor 𝑢𝑝₁ ℊ t

map𝐸𝑙𝑠 : {𝒯 𝒯₁ 𝒯₂ : TyStr ℓ₁} {𝑓 : TyMor 𝒯 𝒯₁} {𝑔 : TyMor 𝒯 𝒯₂} {ℰ₁ : ElStr 𝒯₁ ℓ₂} {ℰ₂ : ElStr 𝒯₂ ℓ₂}
  (𝒻 : ElMor 𝑓 𝑔 ℰ₁ ℰ₂) {Γ : 𝐶𝑡𝑥 𝒯} → 𝐸𝑙𝑠 𝑓 ℰ₁ Γ → 𝐸𝑙𝑠 𝑔 ℰ₂ Γ
𝑢𝑝𝑠₁ : {𝒯 𝒯₁ 𝒯₂ : TyStr ℓ₁} {𝑓 : TyMor 𝒯 𝒯₁} {𝑔 : TyMor 𝒯 𝒯₂} {ℰ₁ : ElStr 𝒯₁ ℓ₂} {ℰ₂ : ElStr 𝒯₂ ℓ₂}
  (𝒻 : ElMor 𝑓 𝑔 ℰ₁ ℰ₂) {Γ : 𝐶𝑡𝑥 𝒯} (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ₁ Γ) → ElMor (𝑠ℎ𝑠 𝑓 ℰ₁ 𝓈s) (𝑠ℎ𝑠 𝑔 ℰ₂ (map𝐸𝑙𝑠 𝒻 𝓈s)) ℰ₁ ℰ₂

map𝐸𝑙𝑠 𝒻 {Γ = ∅} ! = !
map𝐸𝑙𝑠 𝒻 {Γ = Γ ⊹ A} (𝓈s ⊕ 𝓈) = map𝐸𝑙𝑠 𝒻 𝓈s ⊕ 𝑓𝑢𝑛₁ (𝑢𝑝𝑠₁ 𝒻 𝓈s) 𝓈

𝑢𝑝𝑠₁ 𝒻 {Γ = ∅} ! = 𝒻
𝑢𝑝𝑠₁ 𝒻 {Γ = Γ ⊹ A} (𝓈s ⊕ 𝓈) = 𝑢𝑝₁ (𝑢𝑝𝑠₁ 𝒻 𝓈s) 𝓈

map𝐸𝑙𝑠Id : {𝒯₁ 𝒯₂ : TyStr ℓ₁} {𝑓 : TyMor 𝒯₁ 𝒯₂} {ℰ : ElStr 𝒯₂ ℓ₂} {Γ : 𝐶𝑡𝑥 𝒯₁}
  (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ Γ) → map𝐸𝑙𝑠 (idElMor 𝑓 ℰ) 𝓈s ≡ 𝓈s
𝑢𝑝𝑠₁Id : {𝒯₁ 𝒯₂ : TyStr ℓ₁} {𝑓 : TyMor 𝒯₁ 𝒯₂} {ℰ : ElStr 𝒯₂ ℓ₂} {Γ : 𝐶𝑡𝑥 𝒯₁} (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ Γ) →
  PathP (λ i → ElMor (𝑠ℎ𝑠 𝑓 ℰ 𝓈s) (𝑠ℎ𝑠 𝑓 ℰ (map𝐸𝑙𝑠Id 𝓈s i)) ℰ ℰ)
    (𝑢𝑝𝑠₁ (idElMor 𝑓 ℰ) 𝓈s) (idElMor (𝑠ℎ𝑠 𝑓 ℰ 𝓈s) ℰ)

map𝐸𝑙𝑠Id ! = refl
map𝐸𝑙𝑠Id (𝓈s ⊕ 𝓈) i = map𝐸𝑙𝑠Id 𝓈s i ⊕ 𝑓𝑢𝑛₁ (𝑢𝑝𝑠₁Id 𝓈s i) 𝓈

𝑢𝑝𝑠₁Id ! = refl
𝑢𝑝𝑠₁Id(𝓈s ⊕ 𝓈) i = 𝑢𝑝₁ (𝑢𝑝𝑠₁Id 𝓈s i) 𝓈

map𝐸𝑙𝑠² : {𝒯 𝒯₁ 𝒯₂ 𝒯₃ : TyStr ℓ₁} {𝑓 : TyMor 𝒯 𝒯₁} {𝑔 : TyMor 𝒯 𝒯₂} {ℎ : TyMor 𝒯 𝒯₃}
  {ℰ₁ : ElStr 𝒯₁ ℓ₂} {ℰ₂ : ElStr 𝒯₂ ℓ₂} {ℰ₃ : ElStr 𝒯₃ ℓ₂} {Γ : 𝐶𝑡𝑥 𝒯}
  (𝒻 : ElMor 𝑔 ℎ ℰ₂ ℰ₃) (ℊ : ElMor 𝑓 𝑔 ℰ₁ ℰ₂) (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ₁ Γ) →
  map𝐸𝑙𝑠 (𝒻 ∘ElMor ℊ) 𝓈s ≡ map𝐸𝑙𝑠 𝒻 (map𝐸𝑙𝑠 ℊ 𝓈s)
𝑢𝑝𝑠₁∘ : {𝒯 𝒯₁ 𝒯₂ 𝒯₃ : TyStr ℓ₁} {𝑓 : TyMor 𝒯 𝒯₁} {𝑔 : TyMor 𝒯 𝒯₂} {ℎ : TyMor 𝒯 𝒯₃}
  {ℰ₁ : ElStr 𝒯₁ ℓ₂} {ℰ₂ : ElStr 𝒯₂ ℓ₂} {ℰ₃ : ElStr 𝒯₃ ℓ₂} {Γ : 𝐶𝑡𝑥 𝒯}
  (𝒻 : ElMor 𝑔 ℎ ℰ₂ ℰ₃) (ℊ : ElMor 𝑓 𝑔 ℰ₁ ℰ₂) (𝓈s : 𝐸𝑙𝑠 𝑓 ℰ₁ Γ) →
  PathP (λ i → ElMor (𝑠ℎ𝑠 𝑓 ℰ₁ 𝓈s) (𝑠ℎ𝑠 ℎ ℰ₃ (map𝐸𝑙𝑠² 𝒻 ℊ 𝓈s i)) ℰ₁ ℰ₃)
    (𝑢𝑝𝑠₁ (𝒻 ∘ElMor ℊ) 𝓈s)
    (𝑢𝑝𝑠₁ 𝒻 (map𝐸𝑙𝑠 ℊ 𝓈s) ∘ElMor 𝑢𝑝𝑠₁ ℊ 𝓈s)

map𝐸𝑙𝑠² 𝒻 ℊ ! = refl
map𝐸𝑙𝑠² 𝒻 ℊ (𝓈s ⊕ 𝓈) i = map𝐸𝑙𝑠² 𝒻 ℊ 𝓈s i ⊕ 𝑓𝑢𝑛₁ (𝑢𝑝𝑠₁∘ 𝒻 ℊ 𝓈s i) 𝓈

𝑢𝑝𝑠₁∘ 𝒻 ℊ ! = refl
𝑢𝑝𝑠₁∘ 𝒻 ℊ (𝓈s ⊕ 𝓈) i = 𝑢𝑝₁ (𝑢𝑝𝑠₁∘ 𝒻 ℊ 𝓈s i) 𝓈

record WkStr (𝒯 : TyStr ℓ) : Type ℓ where
  coinductive
  field
    𝑤𝑘 : (A : 𝑡𝑦 𝒯) → TyMor 𝒯 (𝑒𝑥 𝒯 A)
    𝑛𝑒𝑥𝑡 : (A : 𝑡𝑦 𝒯) → WkStr (𝑒𝑥 𝒯 A)

open WkStr

𝑛𝑒𝑥𝑡𝑠 : {𝒯 : TyStr ℓ} → WkStr 𝒯 → (Γ : 𝐶𝑡𝑥 𝒯) → WkStr (𝑒𝑥𝑠 𝒯 Γ)
𝑛𝑒𝑥𝑡𝑠 𝒲 ∅ = 𝒲
𝑛𝑒𝑥𝑡𝑠 𝒲 (Γ ⊹ A) = 𝑛𝑒𝑥𝑡 (𝑛𝑒𝑥𝑡𝑠 𝒲 Γ) A

𝑤𝑘𝑠 : {𝒯 : TyStr ℓ} → WkStr 𝒯 → (Γ : 𝐶𝑡𝑥 𝒯) → TyMor 𝒯 (𝑒𝑥𝑠 𝒯 Γ)
𝑤𝑘𝑠 {𝒯 = 𝒯} 𝒲 ∅ = idTyMor 𝒯
𝑤𝑘𝑠 𝒲 (Γ ⊹ A) = 𝑤𝑘 (𝑛𝑒𝑥𝑡𝑠 𝒲 Γ) A ∘TyMor 𝑤𝑘𝑠 𝒲 Γ

record Contextual ℓ₁ ℓ₂ : Type (lsuc (ℓ₁ ⊔ ℓ₂)) where

  field
    𝒯 : TyStr ℓ₁

  ctx = 𝐶𝑡𝑥 𝒯

  field
    ℳ : (Γ : 𝐶𝑡𝑥 𝒯) → ElStr (𝑒𝑥𝑠 𝒯 Γ) ℓ₂
    𝒲 : WkStr 𝒯

  tms : (Γ Δ : ctx) → Type (ℓ₁ ⊔ ℓ₂)
  tms Γ Δ = 𝐸𝑙𝑠 (𝑤𝑘𝑠 𝒲 Γ) (ℳ Γ) Δ

  field
    sub : {Γ Δ : ctx} (σ : tms Γ Δ) → ElMor (𝑤𝑘𝑠 𝒲 Δ) (𝑤𝑘𝑠 𝒲 Γ) (ℳ Δ) (ℳ Γ)

  _⊚_ : {Γ Δ Σ : ctx} → tms Δ Σ → tms Γ Δ → tms Γ Σ
  σ ⊚ τ = map𝐸𝑙𝑠 (sub τ) σ

  field
    𝒾𝒹 : (Γ : ctx) → tms Γ Γ
    𝒾𝒹L : {Γ Δ : ctx} (σ : tms Γ Δ) → 𝒾𝒹 Δ ⊚ σ ≡ σ
    sub𝒾𝒹 : {Γ : ctx} → sub (𝒾𝒹 Γ) ≡ idElMor (𝑤𝑘𝑠 𝒲 Γ) (ℳ Γ)
    sub⊚ : {Γ Δ Σ : ctx} (σ : tms Δ Σ) (τ : tms Γ Δ) → sub (σ ⊚ τ) ≡ sub τ ∘ElMor sub σ

  𝒾𝒹R : {Γ Δ : ctx} (σ : tms Γ Δ) → σ ⊚ 𝒾𝒹 Γ ≡ σ
  𝒾𝒹R {Γ} σ =
    map𝐸𝑙𝑠 (sub (𝒾𝒹 Γ)) σ
      ≡⟨ (λ i → map𝐸𝑙𝑠 (sub𝒾𝒹 i) σ) ⟩
    map𝐸𝑙𝑠 (idElMor (𝑤𝑘𝑠 𝒲 Γ) (ℳ Γ)) σ
      ≡⟨ map𝐸𝑙𝑠Id σ ⟩
    σ
      ∎

  ⊚Assoc : {Γ Δ Σ Ω : ctx} (σ : tms Σ Ω) (τ : tms Δ Σ) (μ : tms Γ Δ) →
    (σ ⊚ τ) ⊚ μ ≡ σ ⊚ (τ ⊚ μ)
  ⊚Assoc σ τ μ =
    map𝐸𝑙𝑠 (sub μ) (map𝐸𝑙𝑠 (sub τ) σ)
      ≡⟨ map𝐸𝑙𝑠² (sub μ) (sub τ) σ ⁻¹ ⟩
    map𝐸𝑙𝑠 (sub μ ∘ElMor sub τ) σ
      ≡⟨ (λ i → map𝐸𝑙𝑠 (sub⊚ τ μ (~ i)) σ) ⟩
    map𝐸𝑙𝑠 (sub (τ ⊚ μ)) σ
      ∎