| Publication | Date of Publication | Type |
|---|
Strict universes for Grothendieck topoi
Theory and Applications of Categories | 2026-06-08 | Paper |
Doubly weak double categories
Applied Categorical Structures | 2026-05-27 | Paper |
| Semantics of multimodal adjoint type theory | 2026-04-02 | Paper |
| Parametricity, automorphisms of the universe, and excluded middle | 2026-02-20 | Paper |
Displayed type theory and semi-simplicial types
Mathematical Structures in Computer Science | 2025-12-30 | Paper |
The univalence principle
Memoirs of the American Mathematical Society | 2025-01-28 | Paper |
| -autonomous envelopes and conservativity | 2025-01-06 | Paper |
Strange new universes: Proof assistants and synthetic foundations
Bulletin of the American Mathematical Society | 2024-04-03 | Paper |
LNL polycategories and doctrines of linear logic
Logical Methods in Computer Science | 2023-08-26 | Paper |
| The derivator of setoids | 2023-01-23 | Paper |
The derivator of setoids
(available as arXiv preprint) | 2023-01-23 | Paper |
AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS
The Bulletin of Symbolic Logic | 2022-10-25 | Paper |
Homotopy Type Theory: A synthetic approach to higher equalities
(available as arXiv preprint) | 2022-10-11 | Paper |
| Strict universes for Grothendieck topoi | 2022-02-24 | Paper |
| The directed plump ordering | 2022-02-15 | Paper |
Magnitude homology of enriched categories and metric spaces
Algebraic & Geometric Topology | 2021-11-24 | Paper |
Homotopy type theory: the logic of space
(available as arXiv preprint) | 2021-11-12 | Paper |
| Homotopy type theory: the logic of space | 2021-11-12 | Paper |
Semantics of higher inductive types
Mathematical Proceedings of the Cambridge Philosophical Society | 2021-09-14 | Paper |
| A practical type theory for symmetric monoidal categories | 2021-08-16 | Paper |
A practical type theory for symmetric monoidal categories
(available as arXiv preprint) | 2021-08-16 | Paper |
Generalized stability for abstract homotopy theories
Annals of \(K\)-Theory | 2021-08-13 | Paper |
| Quantum gauge field theory in cohesive homotopy type theory | 2021-06-23 | Paper |
Quantum gauge field theory in cohesive homotopy type theory
(available as arXiv preprint) | 2021-06-23 | Paper |
Construction of the circle in \textit{UniMath}
Journal of Pure and Applied Algebra | 2021-06-09 | Paper |
| The Univalence Principle | 2021-02-11 | Paper |
A higher structure identity principle
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
| Categories of Nets | 2021-01-11 | Paper |
| scientific article; zbMATH DE number 7204444 (Why is no real title available?) | 2020-05-26 | Paper |
| *-Autonomous Envelopes and Conservativity | 2020-04-17 | Paper |
| The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions | 2020-02-06 | Paper |
The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions
(available as arXiv preprint) | 2020-02-06 | Paper |
Modalities in homotopy type theory
(available as arXiv preprint) | 2020-01-22 | Paper |
| Constructing symmetric monoidal bicategories functorially | 2019-10-21 | Paper |
Construction of the Circle in UniMath
(available as arXiv preprint) | 2019-10-04 | Paper |
| All (\infty,1)-toposes have strict univalent universes | 2019-04-15 | Paper |
A type theory for synthetic -categories
(available as arXiv preprint) | 2019-03-19 | Paper |
Comparing material and structural set theories
Annals of Pure and Applied Logic | 2019-02-04 | Paper |
The linearity of fixed point invariants
New Directions in Homotopy Theory | 2018-10-09 | Paper |
| Contravariance through enrichment | 2018-06-07 | Paper |
Contravariance through enrichment
(available as arXiv preprint) | 2018-06-07 | Paper |
Affine logic for constructive mathematics
(available as arXiv preprint) | 2018-05-19 | Paper |
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
Mathematical Structures in Computer Science | 2018-05-17 | Paper |
Univalence for inverse EI diagrams
Homology, Homotopy and Applications | 2018-01-17 | Paper |
Adjoint logic with a 2-category of modes
Logical Foundations of Computer Science | 2017-07-21 | Paper |
| The Seifert-van Kampen Theorem in Homotopy Type Theory | 2017-07-19 | Paper |
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
Idempotents in intensional type theory
Logical Methods in Computer Science | 2017-04-11 | Paper |
| Parametricity, automorphisms of the universe, and excluded middle | 2017-01-19 | Paper |
Univalent categories and the Rezk completion
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Univalence for inverse diagrams and homotopy canonicity
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
| The linearity of traces in monoidal categories and bicategories | 2016-07-07 | Paper |
The linearity of traces in monoidal categories and bicategories
(available as arXiv preprint) | 2016-07-07 | Paper |
The univalence axiom for elegant Reedy presheaves
Homology, Homotopy and Applications | 2016-02-25 | Paper |
Enriched categories as a free cocompletion
Advances in Mathematics | 2016-01-15 | Paper |
The additivity of traces in monoidal derivators
Journal of \(K\)-Theory | 2015-08-10 | Paper |
| Reedy categories and their generalizations | 2015-07-04 | Paper |
Traces in symmetric monoidal categories
Expositiones Mathematicae | 2014-09-04 | Paper |
Mayer-Vietoris sequences in stable derivators
Homology, Homotopy and Applications | 2014-09-02 | Paper |
Mayer-Vietoris sequences in stable derivators
Homology, Homotopy and Applications | 2014-09-02 | Paper |
The multiplicativity of fixed point invariants
Algebraic & Geometric Topology | 2014-04-09 | Paper |
Shadows and traces in bicategories
Journal of Homotopy and Related Structures | 2013-11-18 | Paper |
Duality and traces for indexed monoidal categories
Theory and Applications of Categories | 2013-09-04 | Paper |
Duality and traces for indexed monoidal categories
Theory and Applications of Categories | 2013-09-04 | Paper |
Enriched indexed categories
Theory and Applications of Categories | 2013-09-04 | Paper |
Enriched indexed categories
Theory and Applications of Categories | 2013-09-04 | Paper |
Exact completions and small sheaves
Theory and Applications of Categories | 2012-10-22 | Paper |
Exact completions and small sheaves
Theory and Applications of Categories | 2012-10-22 | Paper |
| The Shape of Infinity | 2012-09-12 | Paper |
Not every pseudoalgebra is equivalent to a strict one
Advances in Mathematics | 2012-03-02 | Paper |
Enhanced 2-categories and limits for lax morphisms
Advances in Mathematics | 2012-01-04 | Paper |
Comparing composites of left and right derived functors
The New York Journal of Mathematics | 2011-08-02 | Paper |
Comparing composites of left and right derived functors
The New York Journal of Mathematics | 2011-08-02 | Paper |
Comparing composites of left and right derived functors
The New York Journal of Mathematics | 2011-08-02 | Paper |
| A unified framework for generalized multicategories | 2011-08-01 | Paper |
A unified framework for generalized multicategories
(available as arXiv preprint) | 2011-08-01 | Paper |
| A unified framework for generalized multicategories | 2011-08-01 | Paper |
| Stack semantics and the comparison of material and structural set theories | 2010-04-21 | Paper |
| Constructing symmetric monoidal bicategories | 2010-04-06 | Paper |
Lectures on n-categories and cohomology
Towards Higher Categories | 2010-01-18 | Paper |
| Framed bicategories and monoidal fibrations | 2009-11-21 | Paper |
Framed bicategories and monoidal fibrations
(available as arXiv preprint) | 2009-11-21 | Paper |
| Framed bicategories and monoidal fibrations | 2009-11-21 | Paper |
| Set theory for category theory | 2008-10-07 | Paper |
Parametrized spaces model locally constant homotopy sheaves
Topology and its Applications | 2008-02-14 | Paper |
| Homotopy limits and colimits and enriched homotopy theory | 2006-10-05 | Paper |
Semantics of multimodal adjoint type theory
(available as arXiv preprint) | N/A | Paper |
Displayed Type Theory and Semi-Simplicial Types
(available as arXiv preprint) | N/A | Paper |
