| Publication | Date of Publication | Type |
|---|
The Formal Theory of Monads, Univalently
(available as arXiv preprint) | N/A | Paper |
Univalent Enriched Categories and the Enriched Rezk Completion
(available as arXiv preprint) | N/A | Paper |
Insights From Univalent Foundations: A Case Study Using Double Categories
(available as arXiv preprint) | N/A | Paper |
| Initial algebras of domains via quotient inductive-inductive types | 2026-08-11 | Paper |
Univalent enriched categories and the enriched Rezk completion
Logical Methods in Computer Science | 2026-08-04 | Paper |
| Insights from univalent foundations: a case study using double categories | 2026-06-09 | Paper |
| Univalent enriched categories and the enriched rezk completion | 2026-01-14 | Paper |
The formal theory of monads, univalently
Logical Methods in Computer Science | 2025-03-06 | Paper |
| The interval domain in homotopy type theory | 2025-02-07 | Paper |
From Semantics to Syntax: A Type Theory for Comprehension Categories
(available as arXiv preprint) | 2025-01-01 | Paper |
| Semantics for two-dimensional type theory | 2024-12-06 | Paper |
| Certifying higher-order polynomial interpretations | 2024-11-26 | Paper |
| The formal theory of monads, univalently | 2024-10-21 | Paper |
Bicategorical type theory: semantics and syntax
Mathematical Structures in Computer Science | 2024-03-05 | Paper |
The internal languages of univalent categories
(available as arXiv preprint) | 2024-01-01 | Paper |
Intrinsically Correct Sorting in Cubical Agda
(available as arXiv preprint) | 2024-01-01 | Paper |
| Univalent Double Categories | 2023-10-13 | Paper |
Univalent Double Categories
(available as arXiv preprint) | 2023-01-01 | Paper |
Bicategories in univalent foundations
Mathematical Structures in Computer Science | 2022-12-09 | Paper |
Bicategories in univalent foundations
(available as arXiv preprint) | 2022-07-18 | Paper |
| Guarded recursion in Agda via sized types | 2022-07-18 | Paper |
| The construction of set-truncated higher inductive types | 2022-04-29 | Paper |
Constructing higher inductive types as groupoid quotients
(available as arXiv preprint) | 2021-05-25 | Paper |
| Constructing higher inductive types as groupoid quotients | 2021-05-25 | Paper |
Constructing higher inductive types as groupoid quotients
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
Bicategories in Univalent Foundations
(available as arXiv preprint) | 2019-03-04 | Paper |
