nLab
Per MartinLöf
Skip the Navigation Links

Home Page

All Pages

Recently Revised

Authors

Feeds

Export

Wikipedia entry
Related entries
type theory
dependent type theory
,
intensional type theory
identity types
category:
people
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
,
constructive mathematics
,
predicative mathematics
,
type theory
,
propositions as types
,
Wtype
,
identity type
,
inductive type
,
proofs as programs
,
intensional type theory
,
relation between type theory and category theory
,
sequent
,
BuraliForti's paradox
,
judgment
,
natural deduction
,
metalanguage
,
looping combinator
,
meaning explanation