nLab
Martin Hofmann
Skip the Navigation Links

Home Page

All Pages

Recently Revised

Authors

Feeds

Export

webpage
category:
people
Created on November 18, 2011 02:05:39 by
Urs Schreiber
(217.232.18.193)
Edit
 Views:
Print

TeX

Source
 Linked from:
type theory
,
universe
,
categorical semantics
,
homotopy type theory
,
type of types
,
univalence axiom
,
intensional type theory
,
substitution
,
relation between type theory and category theory
,
categorical model of dependent types