×

Lumsdaine, Peter LeFanu

Author ID: lumsdaine.peter-lefanu Recent zbMATH articles by "Lumsdaine, Peter LeFanu"
Published as: Lumsdaine, Peter LeFanu; Lumsdaine, Peter Lefanu; Lefanu Lumsdaine, Peter; Lumsdaine, Peter; LeFanu Lumsdaine, Peter; Lumsdaine, P. L.
Homepage: http://peterlefanulumsdaine.com/
External Links: MGP · ORCID · Google Scholar · MathOverflow · dblp

Publications by Year

Citations contained in zbMATH Open

17 Publications have been cited 176 times in 120 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
The simplicial model of univalent foundations (after Voevodsky). Zbl 1471.18025
Kapulkin, Krzysztof; Lumsdaine, Peter Lefanu
32
2021
An introduction to quantum programming in Quipper. Zbl 1406.68013
Green, Alexander S.; Lumsdaine, Peter LeFanu; Ross, Neil J.; Selinger, Peter; Valiron, Benoît
28
2013
The local universes model: an overlooked coherence construction for dependent type theories. Zbl 1354.03101
Lumsdaine, Peter LeFanu; Warren, Michael A.
25
2015
Weak omega-categories from intensional type theory. Zbl 1250.03127
Lumsdaine, Peter LeFanu
13
2010
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
13
2015
Semantics of higher inductive types. Zbl 1470.18007
Lumsdaine, Peter Lefanu; Shulman, Michael
11
2020
The homotopy theory of type theories. Zbl 1397.18015
Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
11
2018
Weak \(\omega \)-categories from intensional type theory. Zbl 1200.03050
Lumsdaine, Peter LeFanu
8
2009
The law of excluded middle in the simplicial model of type theory. Zbl 1452.03038
Kapulkin, Chris; Lefanu Lumsdaine, Peter
8
2020
Categorical structures for type theory in univalent foundations. Zbl 1496.03053
Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir
6
2018
A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. Zbl 1395.55011
Hou (Favonia), Kuen-Bang; Finster, Eric; Licata, Daniel R.; Lumsdaine, Peter LeFanu
5
2016
Displayed categories. Zbl 1419.18001
Ahrens, Benedikt; Lefanu Lumsdaine, Peter
5
2019
On the Bourbaki-Witt principle in toposes. Zbl 1286.03164
Bauer, Andrej; Lumsdaine, Peter Lefanu
4
2013
Displayed categories. Zbl 1434.18002
Ahrens, Benedikt; Lumsdaine, Peter LeFanu
3
2017
Lawvere-Tierney sheaves in algebraic set theory. Zbl 1183.03068
Awodey, S.; Gambino, N.; Lumsdaine, P. L.; Warren, M. A.
2
2009
Categorical structures for type theory in univalent foundations. Zbl 07204300
Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir
2
2017
The simplicial model of univalent foundations (after Voevodsky). Zbl 1471.18025
Kapulkin, Krzysztof; Lumsdaine, Peter Lefanu
32
2021
Semantics of higher inductive types. Zbl 1470.18007
Lumsdaine, Peter Lefanu; Shulman, Michael
11
2020
The law of excluded middle in the simplicial model of type theory. Zbl 1452.03038
Kapulkin, Chris; Lefanu Lumsdaine, Peter
8
2020
Displayed categories. Zbl 1419.18001
Ahrens, Benedikt; Lefanu Lumsdaine, Peter
5
2019
The homotopy theory of type theories. Zbl 1397.18015
Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
11
2018
Categorical structures for type theory in univalent foundations. Zbl 1496.03053
Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir
6
2018
Displayed categories. Zbl 1434.18002
Ahrens, Benedikt; Lumsdaine, Peter LeFanu
3
2017
Categorical structures for type theory in univalent foundations. Zbl 07204300
Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir
2
2017
A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. Zbl 1395.55011
Hou (Favonia), Kuen-Bang; Finster, Eric; Licata, Daniel R.; Lumsdaine, Peter LeFanu
5
2016
The local universes model: an overlooked coherence construction for dependent type theories. Zbl 1354.03101
Lumsdaine, Peter LeFanu; Warren, Michael A.
25
2015
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
13
2015
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
An introduction to quantum programming in Quipper. Zbl 1406.68013
Green, Alexander S.; Lumsdaine, Peter LeFanu; Ross, Neil J.; Selinger, Peter; Valiron, Benoît
28
2013
On the Bourbaki-Witt principle in toposes. Zbl 1286.03164
Bauer, Andrej; Lumsdaine, Peter Lefanu
4
2013
Weak omega-categories from intensional type theory. Zbl 1250.03127
Lumsdaine, Peter LeFanu
13
2010
Weak \(\omega \)-categories from intensional type theory. Zbl 1200.03050
Lumsdaine, Peter LeFanu
8
2009
Lawvere-Tierney sheaves in algebraic set theory. Zbl 1183.03068
Awodey, S.; Gambino, N.; Lumsdaine, P. L.; Warren, M. A.
2
2009
all top 5

Cited by 171 Authors

9 Ahrens, Benedikt
8 Lumsdaine, Peter LeFanu
7 Kapulkin, Krzysztof
6 Shulman, Michael A.
5 Awodey, Steve
5 Harper, Robert
4 Angiuli, Carlo
4 Buchholtz, Ulrik
4 Coquand, Thierry
4 Díaz-Caro, Alejandro
4 Gambino, Nicola
4 Maggesi, Marco
4 Mörtberg, Anders
4 Pitts, Andrew M.
4 Rijke, Egbert
4 Sattler, Christian
4 Szumiło, Karol
4 van der Weide, Niels
3 Christensen, J. Daniel
3 Licata, Daniel R.
3 North, Paige Randall
3 Scoccola, Luis Nerio
3 Spitters, Bas
3 Sterling, Jonathan
2 Birkedal, Lars
2 Brunerie, Guillaume
2 Clouston, Ranald A.
2 Frumin, Dan
2 Grayson, Daniel Richard
2 Henry, Simon
2 Hirschowitz, André
2 Hou (Favonia), Kuen-Bang
2 Huber, Simon
2 Isaev, Valery
2 Kraus, Nicolai
2 Lafont, Ambroise
2 Moerdijk, Ieke
2 Orton, Ian
2 Paolini, Luca
2 Schäfer, Steven
2 Smolka, Gert
2 Valiron, Benoît
2 Van den Berg, Benno
2 Veltri, Niccolò
2 Vezzosi, Andrea
2 von Raumer, Jakob
2 Warren, Michael Alton
2 Zorzi, Margherita
1 Abel, Andreas M.
1 Ackerman, Nathanael Leedom
1 Alexander, Scott
1 Altenkirch, Thorsten
1 Amini, Jason M.
1 Amoretti, Michele
1 Amy, Matthew
1 Anticoli, Linda
1 Ara, Dimitri
1 Arndt, Peter F.
1 Avigad, Jeremy
1 Bardin, Sébastien
1 Bentzen, Bruno
1 Bezem, Marc
1 Bidlingmaier, Martin E.
1 Bizjak, Aleš
1 Blass, Andreas Raphael
1 Bobot, François
1 Bordg, Anthony
1 Boulier, Simon
1 Castellan, Simon
1 Caterina, Gianluca
1 Cavallo, Evan
1 Chapuran, Thomas E.
1 Chareton, Christophe
1 Chernyavskiĭ, A. Yu.
1 Clairambault, Pierre
1 Cockett, J. Robin B.
1 Cohen, Cyril
1 Comfort, Cole
1 Cottrell, Thomas
1 de Jong, Tom J.
1 De Queiroz, Ruy José Guerra Barretto
1 Doczkal, Christian
1 Doret, S. Charles
1 Dowek, Gilles
1 Dybjer, Peter
1 Džamonja, Mirna
1 Emmenegger, Jacopo
1 Felty, Amy P.
1 Ferrari, Davide
1 Fillion-Gourdeau, François
1 Fiore, Marcelo P.
1 Fu, Peng
1 Fujii, Soichiro
1 Gagna, Andrea
1 Gangle, Rocco
1 Gepner, David
1 Geuvers, Jan Herman
1 Ghilardi, Silvio
1 Gouveia, Maria João
1 Grathwohl, Hans Bugge
...and 71 more Authors

Citations by Year