nLab Peter LeFanu Lumsdaine

Selected writings

On the categorical semantics of homotopy type theory in simplicial sets/ ionfty \ionfty -groupoids:

On higher inductive types in homotopy type theory:

and on their categorical semantics:

with precursors in:

On synthetic homotopy theory in homotopy type theory:

Introducing the functional quantum programming language Quipper:

On the categorical semantics of dependent type theory via comprehension categories:

Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:

On dependent type theory:

category: people

Last revised on February 14, 2023 at 15:14:15. See the history of this page for a list of all contributions to it.