nLab
Per Martin-Löf

Skip the Navigation Links | Home Page | All Pages | Recently Revised | Authors | Feeds | Export |
Revised on February 15, 2012 20:21:52 by Urs Schreiber (131.174.41.4)
Edit | Back in time (1 revision) | See changes | History | Views: Print | TeX | Source | Linked from: equality, predicative mathematics, type theory, propositions as types, identity type, inductive type, proofs as programs, intensional type theory, relation between type theory and category theory, sequent, Burali-Forti's paradox, judgment, natural deduction, metalanguage, looping combinator, meaning explanation