Martin Hyland (Cambridge)

Algebraic Homotopy Theory: Lessons for Type Theory

Abstract:
Constructions in abstract homotopy theory generally have
two ingredients. One is essentially algebraic and is founded
on ideas of enriched category theory. The other is strictly
homotopy theoretic in flavour and typically uses ideas from
the theory of model categories. I shall explore the impact 
for type theory of an approach based on the algebraic ideas.