The effective model structure and ∞-groupoid objects, with Nicola Gambino, Karol Szumiło, and Simon Henry.
Relative induction principles for type theories, with Ambrus Kaposi and Christian Sattler.
Canonicity and homotopy canonicity for cubical type theory, with Thierry Coquand and Simon Huber.
Extended version of an FSCD 2019 paper.
Two-level type theory and applications, with Danil Annenkov, Paolo Capriotti, and Nicolai Kraus.
The constructive Kan-Quillen model structure: two new proofs, with Nicola Gambino and Karol Szumiło.
Constructive homotopy theory of marked semisimplicial sets.
Contains a mistake in Theorem 3.43: semisimplicial sets do not form a cofibration category as defined in the note as (cofibration, weak equivalence)-factorizations do not generally exist (cf. the paragraph at the end of Subsection 3.2). Instead, the notion of cofibration category has to be weakened using a notion of pseudofactorizations (similar to the notion of weak model category). The comparisons between cofibration categories have to be adapted to that notion. The same remark applies to the marked setting.
Idempotent completion of cubes in posets.
Derives the Kapulkin−Voevodsky embedding of simplicial sets into cubical sets (over a certain cube category) from the theory of idempotent completion. This shows moreover that it forms an essential geometric embedding. Updated (by request of Thomas Streicher) to include a proof that both adjunctions are Quillen adjunctions (where cubical sets carry the model structure induced by the CCHM model of HoTT.
Free monad sequences and extension operations (2017).
Written to make the van-Kampen style fibration extension argument in the below work in the algebraic setting. This avoids the use of universes. However, I never found examples of settings that satisfy all exact and presentabilty hypotheses and do not alrady have universes (which allow for a simpler argument). This is an ingredient of replaying the below in the algebraic setting.
The equivalence extension property and model structures.
Gives a criterion for establishing certain model structures. The simplicial and cubical models of homotopy type theory (HoTT) satisfy this criterion, giving rise to model structures underlying those models of HoTT (with types as fibrations and all objects cofibrant). Also shows how to derive the Kan−Quillen model structure on simplicial sets without using topological spaces or combinatorial models for fibrant replacement such as Kan's Ex^{∞}-functor.
Space-valued diagrams, type-theoretically (extended abstract), with Nicolai Kraus.
Contains my proposal for a direct replacement of (prefixes of) the simplex category that has the property that finite prefixes of the simplex category have finite direct replacement.