Peter Lefanu Lumsdaine

Available identifiers

zbMath Open lumsdaine.peter-lefanuMaRDI QIDQ1785778

List of research outcomes

Publication	Date of Publication	Type
Semantics of higher inductive types	2021-09-14	Paper
The simplicial model of univalent foundations (after Voevodsky)	2021-06-10	Paper
Homotopical inverse diagrams in categories with attributes	2020-10-22	Paper
The law of excluded middle in the simplicial model of type theory	2020-09-22	Paper
A general definition of dependent type theories	2020-09-11	Paper
Displayed Categories	2020-05-26	Paper
https://portal.mardi4nfdi.de/entity/Q5111175	2020-05-26	Paper
CONSTRUCTIVE REFLECTIVITY PRINCIPLES FOR REGULAR THEORIES	2020-01-10	Paper
Displayed Categories	2019-03-18	Paper
The homotopy theory of type theories	2018-10-01	Paper
Categorical structures for type theory in univalent foundations	2018-09-26	Paper
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory	2018-04-23	Paper
https://portal.mardi4nfdi.de/entity/Q5271394	2017-07-11	Paper
The Local Universes Model	2017-01-30	Paper
Parametricity, automorphisms of the universe, and excluded middle	2017-01-19	Paper
The HoTT Library: A formalization of homotopy type theory in Coq	2016-10-14	Paper
Homotopy limits in type theory	2016-07-27	Paper
An Introduction to Quantum Programming in Quipper	2013-12-17	Paper
On the Bourbaki-Witt principle in toposes	2013-07-26	Paper
Univalence in Simplicial Sets	2012-03-12	Paper
A Small Observation on Co-categories	2011-08-01	Paper
Weak omega-categories from intensional type theory	2010-09-21	Paper
Lawvere–Tierney sheaves in Algebraic Set Theory	2009-09-29	Paper
Weak ω-Categories from Intensional Type Theory	2009-07-07	Paper

Research outcomes over time

This page was built for person: Peter Lefanu Lumsdaine