%%%%% Syntax %%%%% tp : type. %name tp A. atom : type. %name atom R. term : type. %name term M. t : tp. pi : tp -> (atom -> tp) -> tp. sigma : tp -> (atom -> tp) -> tp. sing : atom -> tp. const : constant -> atom. forall : tp -> atom. app : atom -> term -> atom. pi1 : atom -> atom. pi2 : atom -> atom. at : atom -> term. lam : (atom -> term) -> term. pair : term -> term -> term. %%%%% Substitution %%%%% aasub : (atom -> atom) -> term -> atom -> type. %mode aasub +R +M -M'. aosub : (atom -> atom) -> term -> term -> type. %mode aosub +R +M -M'. sub : (atom -> term) -> term -> term -> type. %mode sub +M +M' -M''. tsub : (atom -> tp) -> term -> tp -> type. %mode tsub +A +M -A'. aasub/closed : aasub ([_] R) _ R. aasub/forall : aasub ([x] forall (A x)) M (forall A') <- tsub A M A'. aosub/var : aosub ([x] x) M M. aasub/app : aasub ([x] app (R x) (M x)) N (app R' M') <- aasub R N R' <- sub M N M'. aosub/app : aosub ([x] app (R x) (M x)) N M1' <- aosub R N (lam M1) <- sub M N M' <- sub M1 M' M1'. aasub/pi1 : aasub ([x] pi1 (R x)) M (pi1 R') <- aasub R M R'. aosub/pi1 : aosub ([x] pi1 (R x)) M M1 <- aosub R M (pair M1 M2). aasub/pi2 : aasub ([x] pi2 (R x)) M (pi2 R') <- aasub R M R'. aosub/pi2 : aosub ([x] pi2 (R x)) M M2 <- aosub R M (pair M1 M2). sub/aa : sub ([x] at (R x)) M (at R') <- aasub R M R'. sub/ao : sub ([x] at (R x)) M M' <- aosub R M M'. sub/lam : sub ([x] lam ([y] M x y)) N (lam ([y] M' y)) <- ({y} sub ([x] M x y) N (M' y)). sub/pair : sub ([x] pair (M1 x) (M2 x)) N (pair M1' M2') <- sub M1 N M1' <- sub M2 N M2'. tsub/t : tsub ([_] t) _ t. tsub/pi : tsub ([x] pi (A x) ([y] B x y)) M (pi A' ([y] B' y)) <- tsub A M A' <- ({y} tsub ([x] B x y) M (B' y)). tsub/sigma : tsub ([x] sigma (A x) ([y] B x y)) M (sigma A' ([y] B' y)) <- tsub A M A' <- ({y} tsub ([x] B x y) M (B' y)). tsub/singa : tsub ([x] sing (R x)) M (sing R') <- aasub R M R'. tsub/singo : tsub ([x] sing (R x)) M (sing R') <- aosub R M (at R'). %%%%% Typing Rules %%%%% kof : constant -> tp -> type. %mode kof +C -A. wf : tp -> type. %mode wf +A. vof : atom -> tp -> type. %mode vof +R -A. aof : atom -> tp -> type. %mode aof +R -A. of : term -> tp -> type. %mode of +M +A. wf/t : wf t. wf/pi : wf (pi A B) <- wf A <- ({x} vof x A -> wf (B x)). wf/sigma : wf (sigma A B) <- wf A <- ({x} vof x A -> wf (B x)). wf/sing : wf (sing R) <- aof R t. aof/const : aof (const C) A <- kof C A <- wf A. qtp : tp -> tp = [a] (pi (pi a ([_] t)) ([_] t)). aof/forall : aof (forall A) (qtp A) <- wf A. aof/var : aof X A <- vof X A <- wf A. aof/app : aof (app R M) B' <- aof R (pi A B) <- of M A <- tsub B M B' <- wf B'. aof/pi1 : aof (pi1 R) A <- aof R (sigma A B). aof/pi2 : aof (pi2 R) (B (pi1 R)) <- aof R (sigma A B). of/at : of (at R) t <- aof R t. of/lam : of (lam M) (pi A B) <- wf A <- ({x} vof x A -> of (M x) (B x)). of/pair : of (pair M N) (sigma A B) <- of M A <- tsub B M B' <- of N B' <- ({x} vof x A -> wf (B x)). of/sing : of (at R) (sing R) <- aof R t. %%%%% Constants %%%%% topen : ctp -> tp -> type. %mode topen +A -B. topen/t : topen ct t. topen/pi : topen (cpi Ac Bc) (pi A ([_] B)) <- topen Ac A <- topen Bc B. kof/i : kof C A' <- ckof C A <- topen A A'. %%%%% Worlds %%%%% %block var : block {x:atom}. %block bind : some {a:tp} block {x:atom} {d:vof x a}. %block ofblock : some {x:atom} {a:tp} block {d:vof x a}.