nLab Peter LeFanu Lumsdaine

• Webpage: http://peterlefanulumsdaine.com

Selected writings

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

• Chris Kapulkin, Peter LeFanu Lumsdaine, The Simplicial Model of Univalent Foundations (after Voevodsky), Journal of the European Mathematical Society 23 (2021) 2071–2126 $[$arXiv:1211.2851, doi:10.4171/jems/1050$]$

On excluded middle in simplicial sets and the compatibility of excluded middle with the univalence axiom:

• Chris Kapulkin, Peter LeFanu Lumsdaine, The law of excluded middle in the simplicial model of type theory (arXiv:2006.13694)

On higher inductive types in homotopy type theory:

• Peter LeFanu Lumsdaine, Higher inductive types, a tour of the menagerie (2011) [blog post]

• Peter LeFanu Lumsdaine, Higher Inductive Types: The circle and friends, axiomatically (2011) [pdf, pdf]

and on their categorical semantics:

• Peter LeFanu Lumsdaine, Mike Shulman, Semantics of higher inductive types, Math. Proc. Camb. Phil. Soc. 169 (2020) 159-208 [arXiv:1705.07088, talk slides pdf, doi:10.1017/S030500411900015X]

with precursors in:

• Mike Shulman, Peter LeFanu Lumsdaine, Semantics of higher inductive types (2012) [pdf]

• Mike Shulman, Peter LeFanu Lumsdaine, Semantics and syntax of higher inductive types (2016) [slides]

On synthetic homotopy theory in homotopy type theory:

• Guillaume Brunerie, Dan Licata, Peter LeFanu Lumsdaine: Homotopy theory in type theory, 2013 (pdf slides, pdf, blog entry 1, blog entry 2)

Introducing the functional quantum programming language Quipper:

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948:110-124, Springer, 2013 (arXiv:1304.5485)

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

• Peter LeFanu Lumsdaine, Michael Warren, The local universes model: An overlooked coherence construction for dependent type theory, ACM Trans. Comput. Log., 16 3 no 23 (2015) 1-31 [arXiv:1411.1736, doi:10.1145/2754931]

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

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

On dependent type theory:

• Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine, A general definition of dependent type theories [arXiv:2009.05539]

Related entries

• initiality conjecture

• univalent foundations of mathematics

• UniMath project

category: people