nLab
Peter LeFanu Lumsdaine
Skip the Navigation Links

Home Page

All Pages

Recently Revised

Authors

Feeds

Export

webpage
category:
people
Revised on November 3, 2011 00:48:25 by
Urs Schreiber
(88.65.212.178)
Edit

Back in time
(1 revision)

See changes

History
 Views:
Print

TeX

Source
 Linked from:
monoidal category
,
Contributors
,
homotopy limit
,
enriched derivator
,
identity type
,
homotopy type theory
,
type of types
,
Coq
,
inductive type
,
function extensionality
,
higher inductive type
,
univalence axiom
,
Oberwolfach HoTTCoq tutorial
,
substitution
,
relation between type theory and category theory
,
categorical model of dependent types
,
BlakersMassey theorem