nLab AUTOMATH

{ —————————– 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)] refltype : eq_type(A,A) := PRIM B * 1:eqtype(A,B) sym_type : eq_type(B,A) := PRIM C * 1:eqtype(A,B) trans_type : eq_type(A,C) := PRIM a * 1:in(a,A)] refl : eqin(a,a,A) := PRIM b * 1:eqin(a,b,A) sym : eq_in(b,a,A) := PRIM c * 1:eqin(a,b,A) trans : eq_in(a,c,A) := PRIM]

B * [a:pterm][_1:in(a,A)][2:eqtype(A,B)] conv_in : in(a,B) := PRIM a * [b:pterm][_1:eq_in(a,b,A)][2:eqtype(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,ptermtype(]

{ —————————– the empty type —————————4– }

• ‘0’ : pterm := PRIM

• [a:pterm] R_0 : pterm := PRIM

• ‘0’form : type(‘0’) := PRIM a * [C:x,ptermpterm] [1:x,ptermtype(]

{ —————————– 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,ptermpterm] [1:x,ptermtype(]

{ —————————– 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’intro1 : in(1,’2’) := PRIM

• ‘2’intro2 : in(2,’2’) := PRIM a * [C:x,ptermpterm] [1:x,ptermtype(]

• [A:pterm][B:pterm][c:pterm][_1:type(A)][2:type(B)]3:in(c,2)] 2elim_type : type(R_2(A,B,c)) := PRIM B * 1:type(A)]2:type(B)] 2eq_type_1 : eq_type(R_2(A,B,1),A) := PRIM 2eqtype_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,ptermpterm] lambda : pterm := PRIM
• [f:pterm][a:pterm] app : pterm := PRIM

B * [C:x,ptermpterm][_1:type(A)][2:x,ptermeqtype(]

B * [1:type(A)]2:x,ptermtype(]

{ —————————– 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,ptermpterm][_1:type(A)][2:x,ptermeqtype(]

B * [1:type(A)]2:x,ptermtype(]

{ —————————– 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,ptermpterm][_1:type(A)][2:x,ptermeqtype(]

B * [1:type(A)]2:x,ptermtype(]

{ —————————– extensionality ————————–10– }

• [A:pterm][a:pterm][b:pterm] Eq : pterm := PRIM b * [1:type(A)]2:in(a,A)]3:in(b,A)] Eqform : type(Eq(A,a,b)) := PRIM b * 1:eqin(a,b,A) Eq_intro : in(star,Eq(A,a,b)) := PRIM b * c:pterm 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)] EQform : type(EQ(A,B)) := PRIM B * 1:eqtype(A,B) EQ_intro : in(star,EQ(A,B)) := PRIM B * c:pterm EQ_elim : eq_type(A,B) := PRIM EQ_eq : eq_in(c,star,EQ(A,B)) := PRIM]