| Publication | Date of Publication | Type |
|---|
| Parametricity, automorphisms of the universe, and excluded middle | 2026-02-20 | Paper |
Semantics of higher inductive types
Mathematical Proceedings of the Cambridge Philosophical Society | 2021-09-14 | Paper |
The simplicial model of univalent foundations (after Voevodsky)
Journal of the European Mathematical Society (JEMS) | 2021-06-10 | Paper |
Homotopical inverse diagrams in categories with attributes
Journal of Pure and Applied Algebra | 2020-10-22 | Paper |
| The law of excluded middle in the simplicial model of type theory | 2020-09-22 | Paper |
The law of excluded middle in the simplicial model of type theory
(available as arXiv preprint) | 2020-09-22 | Paper |
| A general definition of dependent type theories | 2020-09-11 | Paper |
| Displayed Categories | 2020-05-26 | Paper |
| scientific article; zbMATH DE number 7204300 (Why is no real title available?) | 2020-05-26 | Paper |
Constructive reflectivity principles for regular theories
Journal of Symbolic Logic | 2020-01-10 | Paper |
Displayed categories
(available as arXiv preprint) | 2019-03-18 | Paper |
The homotopy theory of type theories
Advances in Mathematics | 2018-10-01 | Paper |
Categorical structures for type theory in univalent foundations
(available as arXiv preprint) | 2018-09-26 | Paper |
A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
| An introduction to \(\mathbb{P}_{\max}\) forcing | 2017-07-11 | Paper |
The local universes model: an overlooked coherence construction for dependent type theories
ACM Transactions on Computational Logic | 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
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
An introduction to quantum programming in Quipper
Reversible Computation | 2013-12-17 | Paper |
On the Bourbaki-Witt principle in toposes
Mathematical Proceedings of the Cambridge Philosophical Society | 2013-07-26 | Paper |
| Univalence in Simplicial Sets | 2012-03-12 | Paper |
| A small observation on co-categories | 2011-08-01 | Paper |
A small observation on co-categories
(available as arXiv preprint) | 2011-08-01 | Paper |
Weak omega-categories from intensional type theory
Logical Methods in Computer Science | 2010-09-21 | Paper |
Lawvere–Tierney sheaves in Algebraic Set Theory
Journal of Symbolic Logic | 2009-09-29 | Paper |
Weak ω-Categories from Intensional Type Theory
Lecture Notes in Computer Science | 2009-07-07 | Paper |
