{-# OPTIONS --allow-unsolved-metas --no-termination-check #-} module TT where module Prelude where -- Props ------------------------------------------------------------------ data True : Set where tt : True data False : Set where postulate falseE : (A : Set) -> False -> A infix 3 _/\_ data _/\_ (P Q : Set) : Set where andI : P -> Q -> P /\ Q -- Zero and One ----------------------------------------------------------- data Zero : Set where data One : Set where unit : One -- Natural numbers -------------------------------------------------------- data Nat : Set where zero : Nat suc : Nat -> Nat _+_ : Nat -> Nat -> Nat zero + m = m suc n + m = suc (n + m) module NatEq where infix 5 _==_ _==_ : Nat -> Nat -> Set zero == zero = True suc n == suc m = n == m _ == _ = False rewriteEq : (C : Nat -> Set){m n : Nat} -> m == n -> C n -> C m rewriteEq C {zero} {zero} _ x = x rewriteEq C {suc _} {suc _} eq x = rewriteEq (\z -> C (suc z)) eq x rewriteEq C {zero} {suc _} () _ rewriteEq C {suc _} {zero} () _ module Chain {A : Set}(_==_ : A -> A -> Set) (_trans_ : {x y z : A} -> x == y -> y == z -> x == z) where infixl 4 _=-=_ infixl 4 _===_ infixr 8 _since_ _=-=_ : (x : A){y : A} -> x == y -> x == y x =-= xy = xy _===_ : {x y z : A} -> x == y -> y == z -> x == z xy === yz = xy trans yz _since_ : {x : A}(y : A) -> x == y -> x == y y since xy = xy module Fin where open Prelude -- Finite sets ------------------------------------------------------------ data Suc (A : Set) : Set where fzero' : Suc A fsuc' : A -> Suc A mutual data Fin (n : Nat) : Set where finI : Fin' n -> Fin n Fin' : Nat -> Set Fin' zero = Zero Fin' (suc n) = Suc (Fin n) fzero : {n : Nat} -> Fin (suc n) fzero = finI fzero' fsuc : {n : Nat} -> Fin n -> Fin (suc n) fsuc i = finI (fsuc' i) finE : {n : Nat} -> Fin n -> Fin' n finE (finI i) = i module FinEq where infix 5 _==_ _==_ : {n : Nat} -> Fin n -> Fin n -> Set _==_ {suc _} (finI fzero' ) (finI fzero' ) = True _==_ {suc _} (finI (fsuc' i)) (finI (fsuc' j)) = i == j _==_ _ _ = False rewriteEq : {n : Nat}(C : Fin n -> Set){i j : Fin n} -> i == j -> C j -> C i rewriteEq {suc _} C {finI fzero' } {finI fzero' } eq x = x rewriteEq {suc _} C {finI (fsuc' i)} {finI (fsuc' j)} eq x = rewriteEq (\z -> C (fsuc z)) eq x rewriteEq {suc _} C {finI (fsuc' _)} {finI fzero' } () _ rewriteEq {suc _} C {finI fzero' } {finI (fsuc' _)} () _ rewriteEq {zero} C {finI ()} {_} _ _ module Vec where open Prelude open Fin infixr 15 _::_ -- Vectors ---------------------------------------------------------------- data Nil : Set where nil' : Nil data Cons (A As : Set) : Set where cons' : A -> As -> Cons A As mutual data Vec (A : Set)(n : Nat) : Set where vecI : Vec' A n -> Vec A n Vec' : Set -> Nat -> Set Vec' A zero = Nil Vec' A (suc n) = Cons A (Vec A n) nil : {A : Set} -> Vec A zero nil = vecI nil' _::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n) x :: xs = vecI (cons' x xs) vecE : {A : Set}{n : Nat} -> Vec A n -> Vec' A n vecE (vecI xs) = xs vec : {A : Set}(n : Nat) -> A -> Vec A n vec zero _ = nil vec (suc n) x = x :: vec n x map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n map {zero} f (vecI nil') = nil map {suc n} f (vecI (cons' x xs)) = f x :: map f xs _!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A _!_ {zero } _ (finI ()) _!_ {suc n} (vecI (cons' x _ )) (finI fzero') = x _!_ {suc n} (vecI (cons' _ xs)) (finI (fsuc' i)) = xs ! i tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n tabulate {zero} f = nil tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x)) module Untyped where open Prelude open Fin open Vec Name = Nat data Expr (n : Nat) : Set where eVar : Fin n -> Expr n eApp : Expr n -> Expr n -> Expr n eLam : Expr (suc n) -> Expr n eSet : Expr n eEl : Expr n ePi : Expr n eCon : Name -> Expr n module ExprEq where infix 5 _==_ _==_ : {n : Nat} -> Expr n -> Expr n -> Set eVar i == eVar j = FinEq._==_ i j eApp e1 e2 == eApp e3 e4 = e1 == e3 /\ e2 == e4 eLam e1 == eLam e2 = e1 == e2 eSet == eSet = True eEl == eEl = True ePi == ePi = True eCon f == eCon g = NatEq._==_ f g _ == _ = False rewriteEq : {n : Nat}(C : Expr n -> Set){r s : Expr n} -> r == s -> C s -> C r rewriteEq C {eVar i } {eVar j } eq x = FinEq.rewriteEq (\z -> C (eVar z)) eq x rewriteEq C {eLam e1 } {eLam e2 } eq x = rewriteEq (\z -> C (eLam z)) eq x rewriteEq C {eSet } {eSet } eq x = x rewriteEq C {eEl } {eEl } eq x = x rewriteEq C {ePi } {ePi } eq x = x rewriteEq C {eCon f } {eCon g } eq x = NatEq.rewriteEq (\z -> C (eCon z)) eq x rewriteEq C {eApp e1 e2} {eApp e3 e4} (andI eq13 eq24) x = rewriteEq (\z -> C (eApp z e2)) eq13 ( rewriteEq (\z -> C (eApp e3 z)) eq24 x ) rewriteEq C {eVar _} {eLam _ } () _ rewriteEq C {eVar _} {eSet } () _ rewriteEq C {eVar _} {eEl } () _ rewriteEq C {eVar _} {eCon _ } () _ rewriteEq C {eVar _} {ePi } () _ rewriteEq C {eVar _} {eApp _ _} () _ rewriteEq C {eLam _} {eVar _ } () _ rewriteEq C {eLam _} {eSet } () _ rewriteEq C {eLam _} {eEl } () _ rewriteEq C {eLam _} {eCon _ } () _ rewriteEq C {eLam _} {ePi } () _ rewriteEq C {eLam _} {eApp _ _} () _ rewriteEq C {eSet } {eLam _ } () _ rewriteEq C {eSet } {eVar _ } () _ rewriteEq C {eSet } {eEl } () _ rewriteEq C {eSet } {eCon _ } () _ rewriteEq C {eSet } {ePi } () _ rewriteEq C {eSet } {eApp _ _} () _ rewriteEq C {eEl } {eLam _ } () _ rewriteEq C {eEl } {eSet } () _ rewriteEq C {eEl } {eVar _ } () _ rewriteEq C {eEl } {eCon _ } () _ rewriteEq C {eEl } {ePi } () _ rewriteEq C {eEl } {eApp _ _} () _ rewriteEq C {eCon _} {eLam _ } () _ rewriteEq C {eCon _} {eSet } () _ rewriteEq C {eCon _} {eEl } () _ rewriteEq C {eCon _} {eVar _ } () _ rewriteEq C {eCon _} {ePi } () _ rewriteEq C {eCon _} {eApp _ _} () _ rewriteEq C {ePi } {eLam _ } () _ rewriteEq C {ePi } {eSet } () _ rewriteEq C {ePi } {eEl } () _ rewriteEq C {ePi } {eCon _ } () _ rewriteEq C {ePi } {eVar _ } () _ rewriteEq C {ePi } {eApp _ _} () _ rewriteEq C {eApp _ _} {eLam _ } () _ rewriteEq C {eApp _ _} {eSet } () _ rewriteEq C {eApp _ _} {eEl } () _ rewriteEq C {eApp _ _} {eCon _ } () _ rewriteEq C {eApp _ _} {ePi } () _ rewriteEq C {eApp _ _} {eVar _ } () _ module Typed where open Prelude open Fin open Vec infixl 15 _&_ infix 13 _!!_ infix 5 _==_ -- Contexts --------------------------------------------------------------- data CSuc (n : Nat) : Set Context' : Nat -> Set Context' zero = Nil Context' (suc n) = CSuc n data Context (n : Nat) : Set data Type {n : Nat}(Γ : Context n) : Set data CSuc n where ext : (Γ : Context n) -> Type Γ -> Context' (suc n) data Context n where ctxI : Context' n -> Context n -- Types ------------------------------------------------------------------ _&_ : {n : Nat}(Γ : Context n) -> Type Γ -> Context (suc n) data Term {n : Nat}(Γ : Context n)(A : Type Γ) : Set data Type {n} Γ where SET : Type Γ Pi : (A : Type Γ) -> Type (Γ & A) -> Type Γ El : Term Γ SET -> Type Γ Γ & A = ctxI (ext Γ A) -- Variables -------------------------------------------------------------- data VarSuc {n : Nat}(Γ : Context n)(B : Type Γ)(A : Type (Γ & B)) : Set Var' : {n : Nat}(Γ : Context n) -> Type Γ -> Set Var' {zero} Γ A = Zero Var' {suc n} (ctxI (ext Γ B)) A = VarSuc Γ B A _==_ : {n : Nat}{Γ : Context n} -> Type Γ -> Type Γ -> Set data Ren {n m : Nat}(Γ : Context n)(Δ : Context m) : Set rename : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ upR : {n : Nat}{Γ : Context n}{A : Type Γ} -> Ren Γ (Γ & A) data Var {n : Nat}(Γ : Context n)(A : Type Γ) : Set data VarSuc {n} Γ B A where vzero_ : A == rename upR B -> Var' (Γ & B) A vsuc_ : (C : Type Γ) -> A == rename upR C -> Var Γ C -> Var' (Γ & B) A data Var {n} Γ A where varI : Var' Γ A -> Var Γ A -- Terms ------------------------------------------------------------------ data Sub {n m : Nat}(Γ : Context n)(Δ : Context m) : Set subst : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ down : {n : Nat}{Γ : Context n}{A : Type Γ} -> Term Γ A -> Sub (Γ & A) Γ data Term {n} Γ A where var : (x : Var Γ A) -> Term Γ A app : {B : Type Γ}{C : Type (Γ & B)} -> Term Γ (Pi B C) -> (t : Term Γ B) -> A == subst (down t) C -> Term Γ A lam : {B : Type Γ}{C : Type (Γ & B)} -> Term (Γ & B) C -> A == Pi B C -> Term Γ A -- Context manipulation --------------------------------------------------- ∅ : Context zero ∅ = ctxI nil' _!!_ : {n : Nat}(Γ : Context n) -> Fin n -> Type Γ _!!_ {zero} _ (finI ()) _!!_ {suc _} (ctxI (ext Γ A)) (finI fzero') = rename upR A _!!_ {suc _} (ctxI (ext Γ A)) (finI (fsuc' i)) = rename upR (Γ !! i) -- Renamings -------------------------------------------------------------- data ConsRen {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set Ren' : {n m : Nat} -> Context n -> Context m -> Set Ren' {zero} {m} (ctxI nil') Δ = Nil Ren' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsRen Γ A Δ data ConsRen {n m} Γ A Δ where extRen' : (ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren' (Γ & A) Δ data Ren {n m} Γ Δ where renI : Ren' Γ Δ -> Ren Γ Δ -- Performing renamings --------------------------------------------------- rename' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ rename ρ SET = SET rename ρ A = rename' ρ A liftR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} -> (ρ : Ren Γ Δ) -> Ren (Γ & A) (Δ & rename ρ A) renameTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ} (ρ : Ren Γ Δ) -> Term Γ A -> Term Δ (rename ρ A) rename' ρ SET = SET rename' ρ (Pi A B) = Pi (rename ρ A) (rename (liftR ρ) B) rename' ρ (El t) = El (renameTerm ρ t) lookupR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} (ρ : Ren Γ Δ)(x : Var Γ A) -> Var Δ (rename ρ A) cong : {n m : Nat}{Γ : Context n}{Δ : Context m}(f : Type Γ -> Type Δ) {A B : Type Γ} -> A == B -> f A == f B _trans_ : {n : Nat}{Γ : Context n}{A B C : Type Γ} -> A == B -> B == C -> A == C renameSubstCommute : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ}{B : Type (Γ & A)} {ρ : Ren Γ Δ}{t : Term Γ A} -> rename ρ (subst (down t) B) == subst (down (renameTerm ρ t)) (rename (liftR ρ) B) renameTerm ρ (var x) = var (lookupR ρ x) renameTerm {_}{_}{_}{_}{A} ρ (app{_}{C} s t eq) = app (renameTerm ρ s) (renameTerm ρ t) (cong (rename ρ) eq trans renameSubstCommute) renameTerm ρ (lam t eq) = lam (renameTerm (liftR ρ) t) (cong (rename ρ) eq) lookupR {zero} _ (varI ()) lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ} (renI (extRen' ρ z)) (varI (vzero_ eq)) = {!!} lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ} (renI (extRen' ρ z)) (varI (vsuc_ C eq x)) = {!!} -- Building renamings ----------------------------------------------------- extRen : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} (ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren (Γ & A) Δ extRen ρ x = renI (extRen' ρ x) _coR_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Ren Δ Θ -> Ren Γ Δ -> Ren Γ Θ liftR {_}{_}{_}{A} ρ = extRen (upR coR ρ) (varI {!!}) idR : {n : Nat} {Γ : Context n} -> Ren Γ Γ idR = {!!} _coR_ = {!!} upR = {!!} -- Substitutions ---------------------------------------------------------- data ConsSub {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set Sub' : {n m : Nat} -> Context n -> Context m -> Set Sub' {zero} {m} (ctxI nil') Δ = Nil Sub' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsSub Γ A Δ data ConsSub {n m} Γ A Δ where extSub' : (σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub' (Γ & A) Δ data Sub {n m} Γ Δ where subI : Sub' Γ Δ -> Sub Γ Δ -- Performing substitution ------------------------------------------------ subst' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ subst σ SET = SET subst σ A = subst' σ A liftS : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} -> (σ : Sub Γ Δ) -> Sub (Γ & A) (Δ & subst σ A) substTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ} -> (σ : Sub Γ Δ) -> Term Γ A -> Term Δ (subst σ A) subst' σ (Pi A B) = Pi (subst σ A) (subst (liftS σ) B) subst' σ (El t) = El (substTerm σ t) subst' σ SET = SET substTerm σ (var x) = {!!} substTerm σ (app s t eq) = {!!} substTerm σ (lam t eq) = {!!} -- Building substitutions ------------------------------------------------- liftS {_}{_}{_}{A} σ = {!!} -- extSub (upS ∘ σ) (var fzero (substCompose upS σ A)) -- Works with hidden args to substCompose when inlined in subst -- but not here. Weird. topS : {n : Nat}{Γ : Context n} -> Sub ∅ Γ topS = subI nil' extSub : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} (σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub (Γ & A) Δ extSub σ t = subI (extSub' σ t) idS : {n : Nat}{Γ : Context n} -> Sub Γ Γ idS {zero} {ctxI nil'} = topS idS {suc _} {ctxI (ext Γ A)} = {!!} -- extSub upS (var fzero refl) convert : {n : Nat}{Γ : Context n}{A B : Type Γ} -> A == B -> Term Γ B -> Term Γ A _∘_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Sub Δ Θ -> Sub Γ Δ -> Sub Γ Θ substCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} (σ : Sub Δ Θ)(δ : Sub Γ Δ)(A : Type Γ) -> subst (σ ∘ δ) A == subst σ (subst δ A) _∘_ {zero} {_}{_} {ctxI nil'} _ _ = topS _∘_ {suc _}{_}{_} {ctxI (ext Γ A)} σ (subI (extSub' δ t)) = extSub (σ ∘ δ) (convert (substCompose σ δ A) (substTerm σ t)) upS : {n : Nat}{Γ : Context n}{A : Type Γ} -> Sub Γ (Γ & A) upS = {!!} substId : {n : Nat}{Γ : Context n}{A : Type Γ} -> subst idS A == A down t = extSub idS (convert substId t) -- Convertibility --------------------------------------------------------- A == B = {!!} refl : {n : Nat}{Γ : Context n}{A : Type Γ} -> A == A refl = {!!} cong f eq = {!!} ab trans bc = {!!} convert eq t = {!!} -- Properties ------------------------------------------------------------- renameId : {n : Nat}{Γ : Context n}{A : Type Γ} -> rename idR A == A renameId = {!!} renameCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} (σ : Ren Δ Θ)(δ : Ren Γ Δ)(A : Type Γ) -> rename (σ coR δ) A == rename σ (rename δ A) renameCompose σ δ A = {!!} substId = {!!} substCompose σ δ A = {!!} renameSubstCommute = {!!}