Intuitionistic Type Theory

A-abstraction A₁ Ap f,x arbitrary element Assume A set assumption axiom of choice C(nil cartesian product Combinatory Logic Definitional equality depend derive disjoint union 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 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 ramified recursion right projection set B(x set forming operations set theory substitution rule sup(a,b suppressing proofs theory of types transfinite induction true C true Wx E A)B(x x₁ yields a canonical Zermelo-Fraenkel set theory Пх є