Free natural model as an HIIT

natmod.agda

{-# OPTIONS --cubical #-}
module natmod where
open import Cubical.Foundations.Prelude

data Ctx : Type
data _⊢_ : Ctx → Ctx → Type
data Ty : Ctx → Type
data Tm : Ctx → Type
-- This is halfway between EAT and GAT.
-- GAT is hard! Why is EAT so easy?

variable
  Γ Δ Θ : Ctx
  σ δ θ τ : Γ ⊢ Δ
  A B : Ty Γ
  a b s t : Tm Γ

infix 3 _⊢_
infixl 5 _∘_
infixl 5 _⟦_⟧ᵗ _⟦_⟧ₜ
infixl 4 _,,_

_⟦_⟧ᵗ' : Ty Γ → Δ ⊢ Γ → Ty Δ
_⟦_⟧ₜ' : Tm Γ → Δ ⊢ Γ → Tm Δ
type' : Tm Γ → Ty Γ

data Ctx where
  -- Is it possible to make univalent in one go?
  -- Or Rezk complete later?

  [] : Ctx
  _,,_ : (Γ : Ctx) → Ty Γ → Ctx

𝔮' : ∀ A → Tm (Γ ,, A)
𝔭' : Γ ,, A ⊢ Γ
_∘'_ : Δ ⊢ Γ → Θ ⊢ Δ → Θ ⊢ Γ
path' : type' (𝔮' A ⟦ σ ⟧ₜ') ≡ (A ⟦ 𝔭' ∘' σ ⟧ᵗ')

data _⊢_ where
  isSet⊢ : isSet (Γ ⊢ Δ)

  _∘_ : Δ ⊢ Γ → Θ ⊢ Δ → Θ ⊢ Γ
  id : ∀ Γ → Γ ⊢ Γ

  assoc : (σ ∘ δ) ∘ τ ≡ σ ∘ (δ ∘ τ)
  idₗ : id Γ ∘ σ ≡ σ
  idᵣ : σ ∘ id Γ ≡ σ

  [] : Γ ⊢ []
  η[] : (f : Γ ⊢ []) → σ ≡ []

  𝔭 : Γ ,, A ⊢ Γ

  ext : (σ : Γ ⊢ Δ) (a : Tm Γ)  -- no pretty syntax
    → type' a ≡ A ⟦ σ ⟧ᵗ'
    → Γ ⊢ Δ ,, A
  𝔭-ext : (p : type' a ≡ A ⟦ σ ⟧ᵗ') → 𝔭 ∘ ext σ a p ≡ σ
  𝔭𝔮 : ext (𝔭' ∘' σ) (𝔮' A ⟦ σ ⟧ₜ') path' ≡ σ

data Tm where
  isSetTm : isSet (Tm Γ)

  -- Functorial action
  _⟦_⟧ₜ : Tm Γ → Δ ⊢ Γ → Tm Δ
  _⟦id⟧ₜ : ∀ t → t ⟦ id Γ ⟧ₜ ≡ t
  _⟦_⟧⟦_⟧ₜ : ∀ t (σ : Δ ⊢ Γ) (τ : Θ ⊢ Δ)
    → t ⟦ σ ∘ τ ⟧ₜ ≡ t ⟦ σ ⟧ₜ ⟦ τ ⟧ₜ

  𝔮 : ∀ A → Tm (Γ ,, A)

  𝔮-ext : (p : type' a ≡ A ⟦ σ ⟧ᵗ') → 𝔮 A ⟦ ext σ a p ⟧ₜ ≡ a

data Ty where
  isSetTy : isSet (Ty Γ)

  -- Functorial action
  _⟦_⟧ᵗ : Ty Γ → Δ ⊢ Γ → Ty Δ
  _⟦id⟧ᵗ : ∀ A → A ⟦ id Γ ⟧ᵗ ≡ A
  _⟦_⟧⟦_⟧ᵗ : ∀ A (σ : Δ ⊢ Γ) (τ : Θ ⊢ Δ)
    → A ⟦ σ ∘ τ ⟧ᵗ ≡ A ⟦ σ ⟧ᵗ ⟦ τ ⟧ᵗ

  -- Typing
  type : Tm Γ → Ty Γ
  type⟦⟧ : type (t ⟦ σ ⟧ₜ) ≡ (type t) ⟦ σ ⟧ᵗ

  type-𝔮 : type (𝔮 A) ≡ A ⟦ 𝔭 ⟧ᵗ

_⟦_⟧ᵗ' = _⟦_⟧ᵗ
_⟦_⟧ₜ' = _⟦_⟧ₜ
type' = type

𝔮' = 𝔮
𝔭' = 𝔭

_∘'_ = _∘_
path' {σ = σ}
  = type⟦⟧
  ∙ cong (_⟦ σ ⟧ᵗ) type-𝔮
  ∙ sym (_ ⟦ _ ⟧⟦ σ ⟧ᵗ)