mltt.agda

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties 
open import Data.Maybe
open import Data.Fin
open import Relation.Nullary.Decidable
open import Data.Product

data Con : ℕ → Set
data Tm : ℕ → Set

infixl 30 _∷_

data Con where
  [] : Con 0
  _∷_ : ∀ {n} → Con n → Tm n → Con (suc n)


infixl 15 _$_

data Tm where
  U : ∀ {n} → Tm n
  ` : ∀ {n} → Fin n → Tm n
  Π : ∀ {n} → Tm n → Tm (suc n) → Tm n
  ƛ : ∀ {n} → Tm (suc n) → Tm n 
  _$_ : ∀ {n} → Tm n → Tm n → Tm n



weak : ∀ {n} → Tm n → Tm (suc n)
weak U = U
weak (` x) = ` (inject₁ x)
weak (Π x bd) = Π (weak x) (weak bd)
weak (ƛ x) = ƛ (weak x)
weak (x $ y) = weak x $ weak y

exts : ∀ {n k} → (Fin n → Fin k) → Fin (suc n) → Fin (suc k)
exts f zero = zero
exts f (suc x) = suc (f x)


rename : ∀ {n k} → (Fin n → Fin k) → Tm n → Tm k
rename f U = U
rename f (` x) = ` (f x)
rename f (Π k b) = Π (rename f k) (rename (exts f) b)
rename f (ƛ x) = ƛ (rename (exts f) x)
rename f (x $ x₁) = (rename f x) $ (rename f x₁)

incr : ∀ {n} → Tm n → Tm (suc n)
incr x = rename suc x

extnd : ∀ {n k} → (Fin n → Tm k) → Fin (suc n) → Tm (suc k)
extnd f zero = ` zero
extnd f (suc x) = incr (f x)

simsub : ∀ {n k} → (Fin n → Tm k) → Tm n → Tm k
simsub f U = U
simsub f (` x) = f x
simsub f (Π x bd) = Π (simsub f x) (simsub (extnd f) bd)
simsub f (ƛ x) = ƛ (simsub (extnd f) x)
simsub f (a $ b) = (simsub f a) $ (simsub f b)

subst-down : ∀ {n} → Tm n → Fin (suc n) → Tm n
subst-down x zero = x
subst-down x (suc i) = ` i

infix 30 _[[_]]
_[[_]] : ∀ {n} → Tm (suc n) → Tm n → Tm n
_[[_]] {n} a s = simsub (subst-down s) a

index : ∀ {n} → Con n → Fin n → Tm n
index (Γ ∷ y) zero = incr y
index (Γ ∷ y) (suc x) = incr (index Γ x)

infix 10 _≣_
data _≣_ : ∀ {n} → Tm n → Tm n → Set where
     ≣refl : ∀ {n} {x : Tm n} → x ≣ x
     ≣sym : ∀ {n} {x y : Tm n} → 
            x ≣ y →
            y ≣ x
     ≣trans : ∀ {n} {x y z : Tm n} →
            x ≣ y →
            y ≣ z →
            x ≣ z
     ≣-pi-β : ∀ {n} {x : Tm (suc n)} {y} →
            (ƛ x) $ y ≣ x [[ y ]]
     ≣-pi-η : ∀ {n} (t : Tm n) →
            t ≣ (ƛ ((incr t) $ (` zero)))
     ≣-appₗ : ∀ {n} {x a b : Tm n} →
            a ≣ b →
            a $ x ≣ b $ x
     ≣-appᵣ : ∀ {n} {x a b : Tm n} →
            a ≣ b →
            x $ a ≣ x $ b



infix 20 _⊢_⦂_
data _⊢_⦂_ : ∀ {n} → Con n → Tm n → Tm n → Set where
     var : ∀ {n Γ ty} {k : Fin n} →
           index {n} Γ k ≡ ty → 
           Γ ⊢ ` k ⦂ ty
     univ : ∀ {n} {Γ : Con n} → Γ ⊢ U ⦂ U
     pi : ∀ {n} {Γ : Con n} {hd : Tm n} {bd : Tm (suc n)} →
          Γ ⊢ hd ⦂ U →
          Γ ∷ hd ⊢ bd ⦂ U →
          Γ ⊢ Π hd bd ⦂ U
     lam : ∀ {n} {Γ : Con n} {bd A B} →
          Γ ⊢ A ⦂ U →
          Γ ∷ A ⊢ B ⦂ U →
          Γ ∷ A ⊢ bd ⦂ B →
          Γ ⊢ ƛ bd ⦂ Π A B
     app : ∀ {n} {Γ : Con n} {f x A B r} →
          Γ ⊢ f ⦂ Π A B →
          Γ ⊢ x ⦂ A →
          B [[ x ]] ≡ r →
          Γ ⊢ f $ x ⦂ r
     convₜ : ∀ {n} {Γ : Con n} {x A B} →
          A ≣ B →
          Γ ⊢ x ⦂ A →
          Γ ⊢ x ⦂ B
     convᵥ : ∀ {n} {Γ : Con n} {x y A} →
          x ≣ y →
          Γ ⊢ x ⦂ A →
          Γ ⊢ y ⦂ A


id : Tm 0
id = ƛ (ƛ (` zero))

idt : Tm 0
idt = Π U (Π (` zero) (` (suc zero)))

id⊢ : [] ⊢ id ⦂ idt
id⊢ = lam univ (pi (var refl) (var refl)) 
          (lam (var refl) (var refl) 
               (var refl))

eq : Tm 0
eq = ƛ (ƛ (ƛ (Π (Π (` (suc (suc zero))) U) 
       (Π (` zero $ ` (suc (suc zero))) 
          (` (suc zero) $ ` (suc (suc zero)))))))

eqt : Tm 0
eqt = Π U (Π (` zero) (Π (` (suc zero)) U))

eq⊢ : [] ⊢ eq ⦂ eqt
eq⊢ = lam univ (pi (var refl) (pi (var refl) univ)) 
          (lam (var refl) (pi (var refl) univ) 
               (lam (var refl) univ 
                    (pi (pi (var refl) univ) 
                        (pi (app (var refl) (var refl) refl) 
                            (app (var refl) (var refl) refl))))) 

postulate
  up : ∀ {Γ x t} →
         [] ⊢ x ⦂ t →
         Γ ⊢ x ⦂ t
  weakr : ∀ {n} {Γ : Con n} {x y t} →
        Γ ⊢ x ⦂ t →
        Γ ∷ y ⊢ incr x ⦂ incr t


rfl : Tm 0
rfl = ƛ (ƛ (ƛ (ƛ (` zero))))

rflt : Tm 0
rflt = Π U (Π (` zero) ((incr (incr eq)) $ (` (suc (zero))) $ (` zero) $ (` zero)))

rfl⊢ : [] ⊢ rfl ⦂ rflt
rfl⊢ = lam univ (pi (var refl) (app (app (app (weakr (weakr eq⊢)) 
           (var refl) refl) (var refl) refl) (var refl) refl)) 
           (lam (var refl) (app (app (app (weakr (weakr eq⊢))
           (var refl) refl) (var refl) refl) (var refl) refl) 
           (convₜ (≣-appₗ (≣-appₗ (≣sym ≣-pi-β))) 
           (convₜ (≣-appₗ (≣sym ≣-pi-β)) 
           (convₜ (≣sym ≣-pi-β) 
           (lam (pi (var refl) univ) (pi (app (var refl) (var refl) refl) 
           (app (var refl) (var refl) refl)) 
           (lam (app (var refl) (var refl) refl) 
           (app (var refl) (var refl) refl) 
           (var refl)))))))