explicit-subst.agda

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything hiding (_,_)

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ·   : Con
  _,_ : Con → Ty → Con

mutual
  infix  4 _⊢⃗_
  infixr 5 _∘_
  infixr 5 _,_
  data _⊢⃗_ : Con → Con → Set where -- substitution
    id : ∀ {A⃗} → A⃗ ⊢⃗ A⃗

    _∘_ : ∀ {A⃗ B⃗ C⃗} → B⃗ ⊢⃗ C⃗ → A⃗ ⊢⃗ B⃗ → A⃗ ⊢⃗ C⃗

    _,_ : ∀ {Γ Δ A} → Γ ⊢⃗ Δ → Γ ⊢ A → Γ ⊢⃗ Δ , A

    π₁ : ∀ {Γ A} → Γ , A ⊢⃗ Γ

    ∘-unitˡ : ∀ {A⃗ B⃗} {ρ : A⃗ ⊢⃗ B⃗} → id ∘ ρ ≡ ρ

    ∘-unitʳ : ∀ {A⃗ B⃗} {ρ : A⃗ ⊢⃗ B⃗} → ρ ∘ id ≡ ρ

    ∘-assoc : ∀ {A⃗ B⃗ C⃗ D⃗} {ρ₁ : A⃗ ⊢⃗ B⃗} {ρ₂ : B⃗ ⊢⃗ C⃗} {ρ₃ : C⃗ ⊢⃗ D⃗}
      → (ρ₃ ∘ ρ₂) ∘ ρ₁ ≡ ρ₃ ∘ (ρ₂ ∘ ρ₁)

    ∘/β : ∀ {A⃗ B⃗ C⃗ C} {ρ : A⃗ ⊢⃗ B⃗} {σ : B⃗ ⊢⃗ C⃗} {t : B⃗ ⊢ C}
      → (σ , t) ∘ ρ ≡ (σ ∘ ρ) , (t [ ρ ])

    π₁/β : ∀ {A⃗ B⃗ B} {ρ : A⃗ ⊢⃗ B⃗} {t : A⃗ ⊢ B}
      → π₁ ∘ (ρ , t) ≡ ρ

    id/δ : ∀ {Γ A} → id {Γ , A} ≡ ↑ , var₀

  ↑ : ∀ {Γ A} → Γ , A ⊢⃗ Γ
  ↑ = π₁

  infix  4 _⊢_
  infix  5 ƛ_
  infixl 6 _∙_
  infixl 7 _[_]
  data _⊢_ : Con → Ty → Set where
    π₂ : ∀ {Γ A} → Γ , A ⊢ A

    sub : ∀ {Γ Δ A} → Δ ⊢ A → Γ ⊢⃗ Δ → Γ ⊢ A

    lam : ∀ {Γ A B} → Γ , A ⊢ B → Γ ⊢ A ⇒ B

    app : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B

    sub-var₀ : ∀ {Γ Δ A} {ρ : Γ ⊢⃗ Δ} {t : Γ ⊢ A} → var₀ [ ρ , t ] ≡ t

    sub-id : ∀ {Γ A} {t : Γ ⊢ A} → t [ id ] ≡ t

    sub-∘ : ∀ {Γ Δ Ξ A} {ρ : Δ ⊢⃗ Ξ} {σ : Γ ⊢⃗ Δ} {t : Ξ ⊢ A}
      → t [ ρ ∘ σ ] ≡ t [ ρ ] [ σ ]

    sub-ƛ : ∀ {Γ Δ A B} {ρ : Γ ⊢⃗ Δ} {t : Δ , A ⊢ B}
      → (ƛ t) [ ρ ] ≡ ƛ t [ (ρ ∘ ↑) , var₀ ]

    sub-∙ : ∀ {Γ Δ A B} {ρ : Γ ⊢⃗ Δ} {t : Δ ⊢ A ⇒ B} {u : Δ ⊢ A}
      → (t ∙ u) [ ρ ] ≡ t [ ρ ] ∙ u [ ρ ]

    ⇒/β : ∀ {Γ A B} (t : Γ , A ⊢ B) (u : Γ ⊢ A)
      → (ƛ t) ∙ u ≡ t [ id , u ]

    ⇒/η : ∀ {Γ A B} (t : Γ ⊢ A ⇒ B)
      → ƛ t [ ↑ ] ∙ var₀ ≡ t

  var₀ : ∀ {Γ A} → Γ , A ⊢ A
  var₀ = π₂

  _[_] : ∀ {Γ Δ A} → Δ ⊢ A → Γ ⊢⃗ Δ → Γ ⊢ A
  _[_] = sub

  ƛ_ : ∀ {Γ A B} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
  ƛ_ = lam

  _∙_ : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  _∙_ = app