syntax.sig

@@ -1,29 +1,17 @@
 nat  : Type
-PTm(VarPTm) : Type
 Tm(VarTm) : Type
 PTag : Type
 TTag : Type
-bool : Type
 
 PL : PTag
 PR : PTag
 TPi : TTag
 TSig : TTag
-
-PAbs : (bind PTm in PTm) -> PTm
-PApp : PTm -> PTm -> PTm
-PPair : PTm -> PTm -> PTm
-PProj : PTag -> PTm -> PTm
-PConst : TTag -> PTm
-PUniv : nat -> PTm
-PBot : PTm
-
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
+Const : TTag -> Tm
 Univ : nat -> Tm
-BVal : bool -> Tm
+Bot : Tm
-Bool : Tm
-If : Tm -> Tm -> Tm -> Tm

theories/compile.v

@@ -15,14 +15,11 @@ Module Compile.
     | Pair a b => Pair (F a) (F b)
     | Proj t a => Proj t (F a)
     | Bot => Bot
-    | If a b c => App (App (F a) (F b)) (F c)
-    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
-    | Bool => Bool
     end.
 
   Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
     F (ren_Tm ξ a)= ren_Tm ξ (F a).
-  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.
+  Proof. move : m ξ. elim : n  / a => //=; scongruence. Qed.
 
   #[local]Hint Rewrite Compile.renaming : compile.
 
@@ -36,8 +33,6 @@ Module Compile.
     - hauto lq:on rew:off.
     - hauto lq:on.
     - hauto lq:on inv:option rew:db:compile unfold:funcomp.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
   Qed.
 
   Lemma substing n b (a : Tm (S n)) :

theories/diagram.txt

@@ -18,25 +18,3 @@ a0 >> a1
 |     |
 v     v
 b0 >> b1
-
-
-prov x (x, x)
-
-prov x b
-
-
-a => b
-
-prov x a
-
-prov y b
-
-prov x c
-prov y c
-
-extract c = x
-extract c = y
-
-prov x b
-
-pr