Intuitionistic Type Theory

A B true A-abstraction arbitrary element Assume A set assume we know assumption axiom of choice C(nil cartesian product Combinatory Logic Definitional equality depend derive disjoint union E-equality E-introduction egory element of C(c elements are formed elimination rule equal canonical elements equal elements equality of sets equality rules Example explain family of sets finite formal rules forms of judgement given hence hypothetical judgement instance introduction rules intuitionistic type theory la Russell left projection List(A MARTIN-LÖF mathematical logic means method N-elimination N₁ N₂ natural numbers Note number class obtain a canonical pd(a Peano axiom predicate logic proof construction proof of B(a prop propositional function prove quantification recursion right projection second rule sequence set B(x set forming operations set theory substitution rule sup(a,b suppressing proofs theory of types transfinite induction true C true yields a canonical Zermelo-Fraenkel set theory Σχ ΧΕ Α χεΑ