#!/usr/local/bin/aut { ----------------------------- pseudoterms ------------------------------1-- } pterm : TYPE := PRIM { ----------------------------- judgements -------------------------------4-- } * [A:pterm] type : TYPE := PRIM * [A:pterm][B:pterm] eq_type : TYPE := PRIM * [a:pterm][A:pterm] in : TYPE := PRIM * [a:pterm][b:pterm][A:pterm] eq_in : TYPE := PRIM { ----------------------------- equality rules ---------------------------8-- } * [A:pterm][a:pterm][b:pterm][c:pterm] A * [B:pterm][C:pterm] A * [_1:type(A)] refl_type : eq_type(A,A) := PRIM B * [_1:eq_type(A,B)] sym_type : eq_type(B,A) := PRIM C * [_1:eq_type(A,B)][_2:eq_type(B,C)] trans_type : eq_type(A,C) := PRIM a * [_1:in(a,A)] refl : eq_in(a,a,A) := PRIM b * [_1:eq_in(a,b,A)] sym : eq_in(b,a,A) := PRIM c * [_1:eq_in(a,b,A)][_2:eq_in(b,c,A)] trans : eq_in(a,c,A) := PRIM B * [a:pterm][_1:in(a,A)][_2:eq_type(A,B)] conv_in : in(a,B) := PRIM a * [b:pterm][_1:eq_in(a,b,A)][_2:eq_type(A,B)] conv_eq_in : eq_in(a,b,B) := PRIM { ----------------------------- congruence rules -------------------------2-- } * [A:pterm][a:pterm][b:pterm][C:[x,pterm]pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(C)][_3:eq_in(a,b,A)] cong_type : eq_type(C,C) := PRIM C * [c:[x,pterm]pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]in(c,C)][_3:eq_in(a,b,A)] cong : eq_in(c,c,C) := PRIM { ----------------------------- the empty type ---------------------------4-- } * '0' : pterm := PRIM * [a:pterm] R_0 : pterm := PRIM * '0'_form : type('0') := PRIM a * [C:[x,pterm]pterm] [_1:[x,pterm][_,in(x,'0')]type(C)][_2:in(a,'0')] '0'_elim : in(R_0(a),C) := PRIM { ----------------------------- the unit type ----------------------------7-- } * '1' : pterm := PRIM * star : pterm := PRIM * [c:pterm][a:pterm] R_1 : pterm := PRIM * '1'_form : type('1') := PRIM * '1'_intro : in(star,'1') := PRIM a * [C:[x,pterm]pterm] [_1:[x,pterm][_,in(x,'1')]type(C)][_2:in(a,'1')][_3:in(c,C)] '1'_elim : in(R_1(c,a),C) := PRIM c * [C:[x,pterm]pterm] [_1:[x,pterm][_,in(x,'1')]type(C)][_2:in(c,C)] '1'_eq : eq_in(R_1(c,star),c,C) := PRIM { ----------------------------- the Booleans ----------------------------13-- } * '2' : pterm := PRIM * 1 : pterm := PRIM * 2 : pterm := PRIM * [c:pterm][d:pterm][a:pterm] R_2 : pterm := PRIM * '2'_form : type('2') := PRIM * '2'_intro_1 : in(1,'2') := PRIM * '2'_intro_2 : in(2,'2') := PRIM a * [C:[x,pterm]pterm] [_1:[x,pterm][_,in(x,'2')]type(C)][_2:in(a,'2')] [_3:in(c,<1>C)][_4:in(d,<2>C)] '2'_elim : in(R_2(c,d,a),C) := PRIM d * [C:[x,pterm]pterm] [_1:[x,pterm][_,in(x,'2')]type(C)][_2:in(c,<1>C)][_3:in(d,<2>C)] '2'_eq_1 : eq_in(R_2(c,d,1),c,<1>C) := PRIM '2'_eq_2 : eq_in(R_2(c,d,2),d,<2>C) := PRIM * [A:pterm][B:pterm][c:pterm][_1:type(A)][_2:type(B)][_3:in(c,'2')] '2'_elim_type : type(R_2(A,B,c)) := PRIM B * [_1:type(A)][_2:type(B)] '2'_eq_type_1 : eq_type(R_2(A,B,1),A) := PRIM '2'_eq_type_2 : eq_type(R_2(A,B,2),B) := PRIM { ----------------------------- product types ----------------------------9-- } * [A:pterm][B:[x,pterm]pterm] Pi : pterm := PRIM A * [B':pterm] arrow : pterm := Pi(A,[x,pterm]B') A * [b:[x,pterm]pterm] lambda : pterm := PRIM * [f:pterm][a:pterm] app : pterm := PRIM B * [C:[x,pterm]pterm][_1:type(A)][_2:[x,pterm][_,in(x,A)]eq_type(B,C)] Pi_cong : eq_type(Pi(A,B),Pi(A,C)) := PRIM B * [b:[x,pterm]pterm][c:[x,pterm]pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]eq_in(b,c,B)] lambda_cong : eq_in(lambda(A,b),lambda(A,c),Pi(A,B)) := PRIM B * [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] Pi_form : type(Pi(A,B)) := PRIM B * [b:[x,pterm]pterm][_1:type(A)][_2:[x,pterm][_,in(x,A)]in(b,B)] Pi_intro : in(lambda(A,b),Pi(A,B)) := PRIM B * [a:pterm][f:pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)][_3:in(f,Pi(A,B))][_4:in(a,A)] Pi_elim : in(app(f,a),B) := PRIM a * [b:[x,pterm]pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]in(b,B)][_3:in(a,A)] Pi_eq {beta} : eq_in(app(lambda(A,b),a),b,B) := PRIM { ----------------------------- sum types -------------------------------11-- } * [A:pterm][B:[x,pterm]pterm] Sigma : pterm := PRIM * [a:pterm][b:pterm] pair : pterm := PRIM a * pi_1 : pterm := PRIM a * pi_2 : pterm := PRIM B * [C:[x,pterm]pterm][_1:type(A)][_2:[x,pterm][_,in(x,A)]eq_type(B,C)] Sigma_cong : eq_type(Sigma(A,B),Sigma(A,C)) := PRIM B * [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] Sigma_form : type(Sigma(A,B)) := PRIM B * [a:pterm][b:pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)][_3:in(a,A)][_4:in(b,B)] Sigma_intro : in(pair(a,b),Sigma(A,B)) := PRIM B * [c:pterm][_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] [_3:in(c,Sigma(A,B))] Sigma_elim_1 : in(pi_1(c),A) := PRIM Sigma_elim_2 : in(pi_2(c),B) := PRIM b * [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)][_3:in(a,A)][_4:in(b,B)] Sigma_eq_1 : eq_in(pi_1(pair(a,b)),a,A) := PRIM Sigma_eq_2 : eq_in(pi_2(pair(a,b)),b,B) := PRIM { ----------------------------- W types ----------------------------------8-- } * [A:pterm][B:[x,pterm]pterm] W : pterm := PRIM * [a:pterm][f:pterm] sup : pterm := PRIM * [b:pterm][e:pterm] rec : pterm := PRIM B * [C:[x,pterm]pterm][_1:type(A)][_2:[x,pterm][_,in(x,A)]eq_type(B,C)] W_cong : eq_type(W(A,B),W(A,C)) := PRIM B * [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] W_form : type(W(A,B)) := PRIM B * [a,pterm][f:pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)][_3:in(a,A)] [_4:in(f,arrow(B,W(A,B)))] W_intro : in(sup(a,f),W(A,B)) := PRIM B * [C:[z,pterm]pterm] [x:pterm][u:pterm] D : pterm := arrow(Pi(B,[y,pterm]C),C) C * [b:pterm][e:pterm] [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] [_3:[z,pterm][_,in(z,W)]type(C)] [_4:in(b,Pi(A,[x,pterm]Pi(arrow(B,W),[u,pterm]D(x,u))))][_5:in(e,W)] W_elim : in(rec(b,e),C) := PRIM b * [a:pterm][f:pterm] g : pterm := lambda(B,[y,pterm]rec(b,app(f,y))) [_1:type(A)][_2:[x,pterm][_,in(x,A)]type(B)] [_3:[z,pterm][_,in(z,W)]type(C)] [_4:in(b,Pi(A,[x,pterm]Pi(arrow(B,W),[u,pterm]D(x,u))))] [_5:in(a,A)][_6:in(f,arrow(B,W))] W_eq : eq_in(rec(b,sup(a,f)),app(app(app(b,a),f),g),C) := PRIM { ----------------------------- extensionality --------------------------10-- } * [A:pterm][a:pterm][b:pterm] Eq : pterm := PRIM b * [_1:type(A)][_2:in(a,A)][_3:in(b,A)] Eq_form : type(Eq(A,a,b)) := PRIM b * [_1:eq_in(a,b,A)] Eq_intro : in(star,Eq(A,a,b)) := PRIM b * [c:pterm][_1:in(c,Eq(A,a,b))] Eq_elim : eq_in(a,b,A) := PRIM Eq_eq : eq_in(c,star,Eq(A,a,b)) := PRIM A * [B:pterm] EQ : pterm := PRIM B * [_1:type(A)][_2:type(B)] EQ_form : type(EQ(A,B)) := PRIM B * [_1:eq_type(A,B)] EQ_intro : in(star,EQ(A,B)) := PRIM B * [c:pterm][_1:in(c,EQ(A,B))] EQ_elim : eq_type(A,B) := PRIM EQ_eq : eq_in(c,star,EQ(A,B)) := PRIM