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
https://portal.mardi4nfdi.de/entity/Q5111175	2020-05-26	Paper
https://portal.mardi4nfdi.de/entity/Q5111300	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Peter LeFanu Lumsdaine