137 citations · 500 across the 20 of their papers we have counts for
21 papers
Comparing semantic frameworks for dependently-sorted algebraic theories
Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North
Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using ca…
A general definition of dependent type theories
Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and…
The law of excluded middle in the simplicial model of type theory
Chris Kapulkin, Peter LeFanu Lumsdaine
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.
Homotopical inverse diagrams in categories with attributes
Chris Kapulkin, Peter LeFanu Lumsdaine
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes and an ordered homotopica…
Semantics of higher inductive types
Peter LeFanu Lumsdaine, Mike Shulman
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have prove…
Categorical structures for type theory in univalent foundations
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categori…
Displayed Categories
Benedikt Ahrens, Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having…
Parametricity, automorphisms of the universe, and excluded middle
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine +1
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assumin…
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…
The homotopy theory of type theories
Chris Kapulkin, Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on ). This presents an -category of su…
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present…
Constructive reflectivity principles for regular theories
Henrik Forssell, Peter LeFanu Lumsdaine
Classically, any structure for a signature may be completed to a model of a desired regular theory by means of the chase construction or small object argument. Moreover, th…
The local universes model: an overlooked coherence construction for dependent type theories
Peter LeFanu Lumsdaine, Michael A. Warren
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, depe…
An Introduction to Quantum Programming in Quipper
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross +2
Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial introduction to the language, through a demonstration of…
Quipper: A Scalable Quantum Programming Language
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross +2
The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the…
Homotopy limits in type theory
Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges…
The Simplicial Model of Univalent Foundations (after Voevodsky)
Chris Kapulkin, Peter LeFanu Lumsdaine
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categori…
Univalence in Simplicial Sets
Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.
On the Bourbaki-Witt Principle in Toposes
Andrej Bauer, Peter LeFanu Lumsdaine
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. W…
Weak omega-categories from intensional type theory
Peter LeFanu Lumsdaine
We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely…
Lawvere-Tierney sheaves in algebraic set theory
Steve Awodey, Nicola Gambino, Peter L. Lumsdaine +1
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we c…