\graph Z3

\sorts Prop, Set, Term

\open syntax \* [1] 2.1. *\

   \decl "logical false" False : *Prop

   \decl "logical conjunction" And : [p:*Prop, q:*Prop] *Prop

   \decl "logical disjunction" Or : [p:*Prop, q:*Prop] *Prop

   \decl "logical implication" Imp : [p:*Prop, q:*Prop] *Prop

   \decl "logical comprehension" All : [p:[x:*Set]*Prop] *Prop

   \decl "logical existence" Ex : [p:[x:*Set]*Prop] *Prop

   \decl "syntactical identity" Id : [x:*Set, y:*Set] *Prop

   \decl "rule application" App : [f:*Set, x:*Set, y:*Set] *Prop

   \decl "classification predicate" Cl : [a:*Set] *Prop

   \decl "classification membership" Eta : [x:*Set, a:*Set] *Prop

   \decl "object-to-term-coercion" T : [x:*Set] *Term

   \decl "term application" At : [t:*Term, u:*Term] *Term

   \decl "term-object equivalence" E : [t:*Term, x:*Set] *Prop

\close

\open non_logical_axioms

   \decl "E: reflexivity" e_refl : [x:*Set] E(T(x), x)

\close