mltt.agda

module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data Tm : ℕ → Set where
  var   : ∀ {n} → F.Fin n → Tm n
  app   : ∀ {n} → Tm n → Tm n → Tm n
  lam   : ∀ {n} → Tm (suc n) → Tm n
  Π     : ∀ {n} → Tm n → Tm (suc n) → Tm n
  sig   : ∀ {n} → Tm n → Tm (suc n) → Tm n
  pair  : ∀ {n} → Tm n → Tm n → Tm n
  split : ∀ {n} → Tm n → Tm (suc (suc n)) → Tm n
  U     : ∀ {n} → Tm n

weakenTm : {n : ℕ}(m : ℕ) → Tm n → Tm (n + m)
weakenTm m (var x) = var (F.inject+ m x)
weakenTm m (app tm tm₁) = app (weakenTm m tm) (weakenTm m tm₁)
weakenTm m (lam tm) = lam (weakenTm m tm)
weakenTm m (Π l r) = Π (weakenTm m l) (weakenTm m r)
weakenTm m (sig l r) = sig (weakenTm m l) (weakenTm m r)
weakenTm m (pair tm tm₁) = pair (weakenTm m tm) (weakenTm m tm₁)
weakenTm m (split l r) = split (weakenTm m l) (weakenTm m r)
weakenTm m U = U

bumpTm : {n : ℕ} → Tm n → Tm (suc n)
bumpTm = go zero where
  go : {n : ℕ}(lower : ℕ) → Tm n → Tm (suc n)
  go lower (var x) with lower ≤? F.toℕ x
  ... | yes _ = var (F.suc x)
  ... | no _ = var (F.inject₁ x)
  go lower (app tm tm₁) = app (go lower tm) (go lower tm₁)
  go lower (lam e) = lam (go (suc lower) e)
  go lower (Π l r) = Π (go lower l) (go (suc lower) r)
  go lower (sig l r) = sig (go lower l) (go (suc lower) r)
  go lower (pair tm tm₁) = pair (go lower tm) (go lower tm₁)
  go lower (split l r) = split (go lower l) (go (suc (suc lower)) r)
  go lower U = U

pushDown : {C : Set}{n : ℕ} → C → F.Fin (suc n) → C ⊎ F.Fin n
pushDown c F.zero = inj₁ c
pushDown c (F.suc F.zero) = inj₂ F.zero
pushDown c (F.suc (F.suc m)) with pushDown c (F.suc m)
... | inj₁ x = inj₁ x
... | inj₂ y = inj₂ (F.suc y)

substTm : {m : ℕ} → Tm m → Tm (suc m) → Tm m
substTm = go where
  go : {m : ℕ} → Tm m → Tm (suc m) → Tm m
  go new (var x) with pushDown new x
  ... | inj₁ c = c
  ... | inj₂ x' = var x'
  go new (app e e₁) = app (go new e) (go new e₁)
  go new (lam e) = lam (go (bumpTm new) e)
  go new (Π e e₁) = Π (go new e) (go (bumpTm new) e₁)
  go new (sig e e₁) = sig (go new e) (go (bumpTm new) e₁)
  go new (pair e e₁) = pair (go new e) (go new e₁)
  go new (split e e₁) = split (go new e) (go (bumpTm (bumpTm new)) e₁)
  go new U = U

T : Set
T = Tm 0

data Canon : Set where
  lam   : Tm 1 → Canon
  Π     : T → Tm 1 → Canon
  sig   : T → Tm 1 → Canon
  pair  : T → T → Canon
  U     : Canon

canon2tm : Canon → T
canon2tm (lam x) = lam x
canon2tm (Π x x₁) = Π x x₁
canon2tm (sig x x₁) = sig x x₁
canon2tm (pair x x₁) = pair x x₁
canon2tm U = U

data Eval : T → Canon → Set where
  lam   : ∀ {e} → Eval (lam e) (lam e)
  Π     : ∀ {e e₁} → Eval (Π e e₁) (Π e e₁)
  sig   : ∀ {e e₁} → Eval (sig e e₁) (sig e e₁)
  pair  : ∀ {e e₁} → Eval (pair e e₁) (pair e e₁)
  split : ∀ {e e₁ l r v}
        → Eval e (pair l r)
        → Eval (substTm r (substTm (weakenTm 1 l) e₁)) v
        → Eval (split e e₁) v
  app   : ∀ {e e₁ b v}
        → Eval e (lam b)
        → Eval (substTm e₁ b) v
        → Eval (app e e₁) v
  U     : Eval U U

-- | This lemma is interesting if we had not fixed an order of evaluation
-- on things like split and app. We did so it's just recurse and rewrite.
deterministic : ∀{c c₁} → (e : T) → Eval e c → Eval e c₁ → c ≡ c₁
deterministic (var ()) ev ev₁
deterministic (app e e₁) (app ev ev₁) (app ev₂ ev₃) with deterministic e ev ev₂
... | refl with deterministic _ ev₁ ev₃
... | refl = refl
deterministic (lam e) lam lam = refl
deterministic U U U = refl
deterministic (Π e e₁) Π Π = refl
deterministic (sig e e₁) sig sig = refl
deterministic (pair e e₁) pair pair = refl
deterministic (split e e₁) (split ev ev₁) (split ev₂ ev₃) with deterministic e ev ev₂
... | refl with deterministic _ ev₁ ev₃
... | refl = refl

-- | (λx.x)(λx.x) ⇒ λx.x
test : Eval (app (lam (var F.zero)) (lam (var F.zero))) (lam (var F.zero))
test = app lam lam

data Context : ℕ → Set where
  nil  : Context 0
  cons : ∀ {n} → Context n → Tm n → Context (suc n)

-- | Given a canonical value we can push it through a context
-- to remove one entry of the context. This is tricky due to
-- the dependency between everything.
substContext : ∀ {n} → Canon → Context (suc n) → Context n
substContext c (cons nil x) = nil
substContext {suc n} c (cons (cons cxt x) x₁) =
  cons (substContext c (cons cxt x)) x₁'
  where x₁' = substTm (weakenTm n (canon2tm c)) x₁

data type : Canon → Set
data _∷_ : Canon → Canon → Set
data _∈_[_] : {n : ℕ} → Tm n → Tm n → Context n → Set

data type where
  is-type : ∀ {c} → c ∷ U → type c

data _∷_ where
  pair : ∀ {e e₁ t t₁}
       → e ∈ t [ nil ]
       → e₁ ∈ substTm e t₁ [ nil ]
       → pair e e₁ ∷ sig t t₁
  lam  : ∀ {b t t₁}
       → b ∈ t₁ [ cons nil t ]
       → lam b ∷ Π t t₁
  sig  : ∀ {t t₁}
       → t ∈ U [ nil ]
       → t₁ ∈ U [ cons nil t ]
       → sig t t₁ ∷ U
  Π    : ∀ {t t₁}
       → t ∈ U [ nil ]
       → t₁ ∈ U [ cons nil t ]
       → Π t t₁ ∷ U

splitSubst : ∀ {n} → Tm (suc n) → Tm (suc (suc n))
splitSubst = go 0 where
  go : ∀ {n} → ℕ → Tm (suc n) → Tm (suc (suc n))
  go target (var x) with F.toℕ x ≤? target | target ≤? F.toℕ x
  ... | yes p | yes p₁ = pair (var F.zero) (var (F.suc F.zero))
  ... | yes p | no ¬p  = {!!}
  ... | no ¬p | yes p  = {!!}
  ... | no ¬p | no ¬p₁ = {!!}
  go target (app e e₁) = {!!}
  go target (lam e) = {!!}
  go target (Π e e₁) = {!!}
  go target (sig e e₁) = {!!}
  go target (pair e e₁) = {!!}
  go target (split e e₁) = {!!}
  go target U = {!!}

data _∈_[_] where
  pair : {n : ℕ}{cxt : Context n} → ∀ {e e₁ t t₁}
       → e ∈ t [ cxt ]
       → e₁ ∈ substTm e t₁ [ cxt ]
       → pair e e₁ ∈ sig t t₁ [ cxt ]
  lam  : {n : ℕ}{cxt : Context n} → ∀ {b t t₁}
       → b ∈ t₁ [ cons cxt t ]
       → lam b ∈ Π t t₁ [ cxt ]
  sig  : {n : ℕ}{cxt : Context n} → ∀ {t t₁}
       → t ∈ U [ cxt ]
       → t₁ ∈ U [ cons cxt t ]
       → sig t t₁ ∈ U [ cxt ]
  Π    : {n : ℕ}{cxt : Context n} → ∀ {t t₁}
       → t ∈ U [ cxt ]
       → t₁ ∈ U [ cons cxt t ]
       → Π t t₁ ∈ U [ cxt ]
  split : {n : ℕ}{cxt : Context n} → ∀ {e e₁ t t₁ t₂}
         → e ∈ sig t t₁ [ cxt ]
         → e₁ ∈ substTm t₂ (weakenTm n (pair (var (F.suc F.zero)) (weakenTm 2 (var F.zero)))) [ cons (cons cxt t) t₁ ]
         → split e e₁ ∈ {!!} [ cxt ]