inductive-recursive-term.agda

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

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

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

infix 4 _∋_
data _∋_ : Con → Ty → Set where
  zero : ∀ {Γ A}           → Γ , A ∋ A
  suc  : ∀ {Γ A B} → Γ ∋ A → Γ , B ∋ A

mutual
  infix 4 _⊢⃗_
  data _⊢⃗_ (Γ : Con) : Con → Set where
    ·   : Γ ⊢⃗ ·
    _,_ : ∀ {A⃗ A} → Γ ⊢⃗ A⃗ → Γ ⊢ A → Γ ⊢⃗ A⃗ , A

  infix 4 _⊢_
  data _⊢_ (Γ : Con) : Ty → Set where
    var : ∀ {A} → Γ ∋ A → Γ ⊢ A

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

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

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

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

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

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

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

  infix 4 _≽_
  data _≽_ : Con → Con → Set where
    done : · ≽ ·
    skip : ∀ {Γ Δ A} → Γ ≽ Δ → Γ , A ≽ Δ
    keep : ∀ {Γ Δ A} → Γ ≽ Δ → Γ , A ≽ Δ , A

  idʷ : ∀ {Γ} → Γ ≽ Γ
  idʷ {·    } = done
  idʷ {Γ , A} = keep idʷ

  ↑ʷ : ∀ {Γ A} → Γ , A ≽ Γ
  ↑ʷ = skip idʷ

  ren∋ : ∀ {Γ Δ} → Γ ≽ Δ → ∀ {A} → Δ ∋ A → Γ ∋ A
  ren∋ (skip w) x       = suc (ren∋ w x)
  ren∋ (keep w) zero    = zero
  ren∋ (keep w) (suc x) = suc (ren∋ w x)

  ren⊢ : ∀ {Γ Δ} → Γ ≽ Δ → ∀ {A} → Δ ⊢ A → Γ ⊢ A
  ren⊢ w (var x  ) = var (ren∋ w x)
  ren⊢ w (lam t  ) = lam (ren⊢ (keep w) t)
  ren⊢ w (app t u) = app (ren⊢ w t) (ren⊢ w u)
  ren⊢ w (⇒/η t   i) = {!!}
  ren⊢ w (⇒/β t u i) = {!!}

  infixl 7 _[_]ʷ
  _[_]ʷ : ∀ {Γ Δ A} → Δ ⊢ A → Γ ≽ Δ → Γ ⊢ A
  t [ w ]ʷ = ren⊢ w t

  _∘⌜_⌝ : ∀ {Γ Δ Ξ} → Δ ⊢⃗ Ξ → Γ ≽ Δ → Γ ⊢⃗ Ξ
  ·       ∘⌜ w ⌝ = ·
  (ρ , t) ∘⌜ w ⌝ = ρ ∘⌜ w ⌝ , ren⊢ w t

  ⌜_⌝∘_ : ∀ {Γ Δ Ξ} → Δ ≽ Ξ → Γ ⊢⃗ Δ → Γ ⊢⃗ Ξ
  ⌜ done   ⌝∘ ·       = ·
  ⌜ skip w ⌝∘ (ρ , t) = ⌜ w ⌝∘ ρ
  ⌜ keep w ⌝∘ (ρ , t) = ⌜ w ⌝∘ ρ , t

  done′ : · ⊢⃗ ·
  done′ = ·

  skip′ : ∀ {Γ Δ A} → Γ ⊢⃗ Δ → Γ , A ⊢⃗ Δ
  skip′ ρ = ρ ∘⌜ ↑ʷ ⌝

  keep′ : ∀ {Γ Δ A} → Γ ⊢⃗ Δ → Γ , A ⊢⃗ Δ , A
  keep′ ρ = skip′ ρ , var₀

  ⌜_⌝ : ∀ {Γ Δ} → Γ ≽ Δ → Γ ⊢⃗ Δ
  ⌜ done ⌝   = done′
  ⌜ skip w ⌝ = skip′ ⌜ w ⌝
  ⌜ keep w ⌝ = keep′ ⌜ w ⌝

  id : ∀ {Γ} → Γ ⊢⃗ Γ
  id = ⌜ idʷ ⌝

  sub∋ : ∀ {Γ Δ} → Γ ⊢⃗ Δ → ∀ {A} → Δ ∋ A → Γ ⊢ A
  sub∋ (ρ , t) zero    = t
  sub∋ (ρ , t) (suc x) = sub∋ ρ x

  sub⊢ : ∀ {Γ Δ} → Γ ⊢⃗ Δ → ∀ {A} → Δ ⊢ A → Γ ⊢ A
  sub⊢ ρ (var x  ) = sub∋ ρ x
  sub⊢ ρ (lam t  ) = lam (sub⊢ (keep′ ρ) t)
  sub⊢ ρ (app t u) = app (sub⊢ ρ t) (sub⊢ ρ u)
  sub⊢ ρ (⇒/η t   i) = {!!}
  sub⊢ ρ (⇒/β t u i) = {!!}

  infixl 7 _[_]
  _[_] : ∀ {Γ Δ A} → Δ ⊢ A → Γ ⊢⃗ Δ → Γ ⊢ A
  t [ ρ ] = sub⊢ ρ t