| Publication | Date of Publication | Type |
|---|
| Examples and cofibrant generation of effective Kan fibrations | 2025-01-27 | Paper |
| Apartness and the elimination of strong forms of extensionality | 2023-10-25 | Paper |
| Conservativity of Type Theory over Higher-order Arithmetic | 2023-08-29 | Paper |
| Arrow algebras | 2023-08-27 | Paper |
| Converse extensionality and apartness | 2023-01-09 | Paper |
| Effective Kan fibrations in simplicial sets | 2022-11-08 | Paper |
| A topos for continuous logic | 2022-09-19 | Paper |
| No-go theorems for functorial localic spectra of noncommutative rings | 2021-04-27 | Paper |
| Effective Kan fibrations in simplicial sets | 2020-09-26 | Paper |
| A note on equality in finite‐type arithmetic | 2020-04-29 | Paper |
| Univalent polymorphism | 2020-04-14 | Paper |
| A Kuroda-style \(j\)-translation | 2019-07-04 | Paper |
| A homotopy-theoretic model of function extensionality in the effective topos | 2019-03-12 | Paper |
| Reverse mathematics and parameter-free transfer | 2018-12-18 | Paper |
| Univalent completion | 2018-08-23 | Paper |
| Path Categories and Propositional Identity Types | 2018-08-20 | Paper |
| Exact completion of path categories and algebraic set theory. I: Exact completion of path categories | 2018-05-11 | Paper |
| Arithmetical conservation results | 2018-01-12 | Paper |
| W-types in homotopy-type theory – CORRIGENDUM | 2018-01-04 | Paper |
| The strength of countable saturation | 2017-09-15 | Paper |
| Nonstandard functional interpretations and categorical models | 2017-08-17 | Paper |
| W-types in homotopy type theory | 2016-07-27 | Paper |
| Topological and Simplicial Models of Identity Types | 2015-09-17 | Paper |
| Reverse Mathematics and parameter-free Transfer | 2014-09-24 | Paper |
| The axiom of multiple choice and models for constructive set theory | 2014-09-05 | Paper |
| Hilbert and proof theory | 2014-08-28 | Paper |
| Extending obstructions to noncommutative functorial spectra | 2014-08-25 | Paper |
| A note on arithmetic in finite types | 2014-08-15 | Paper |
| The Herbrand topos | 2013-09-02 | Paper |
| Are there enough injective sets? | 2013-06-27 | Paper |
| Non-deterministic inductive definitions | 2013-02-15 | Paper |
| Erratum to: Noncommutativity as a colimit | 2013-02-01 | Paper |
| A topos for a nonstandard functional interpretation | 2013-01-16 | Paper |
| Noncommutativity as a colimit | 2012-12-21 | Paper |
| Aspects of predicative algebraic set theory III: sheaves | 2012-11-30 | Paper |
| A functional interpretation for nonstandard arithmetic | 2012-10-11 | Paper |
| Derived rules for predicative set theory: an application of sheaves | 2012-09-06 | Paper |
| Predicative toposes | 2012-07-04 | Paper |
| Aspects of predicative algebraic set theory. II: Realizability | 2011-05-10 | Paper |
| Types are weak ω -groupoids | 2011-03-02 | Paper |
| A Unified Approach to Algebraic Set Theory | 2010-01-13 | Paper |
| Three extensional models of type theory | 2009-05-06 | Paper |
| Aspects of predicative algebraic set theory. I: Exact completion | 2008-12-05 | Paper |
| W-types in sheaves | 2008-10-14 | Paper |
| Models of non-well-founded sets via an indexed final coalgebra theorem | 2007-10-17 | Paper |
| Non-well-founded trees in categories | 2007-04-18 | Paper |
| Sheaves for predicative toposes | 2005-07-22 | Paper |
| Inductive types and exact completion | 2005-06-23 | Paper |
| Examples and cofibrant generation of effective Kan fibrations | N/A | Paper |
| The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems | N/A | Paper |
