A constructive model of HoTT for homotopy types (June 2023).
Natural numbers from integers (2023, updated 2024), with David Wärn.
Relative elegance and cartesian cubes with one connection (2022), with Evan Cavallo.
Relative induction principles for type theories (2021), with Rafaël Bocquet and Ambrus Kaposi.
Cubical models of (∞, 1)-categories (2020), with Brandon Doherty, Chris Kapulkin, and Zachery Lindsey (to appear in Memoirs of the American Mathematical Society).
Cylindrical model structures (draft, last updated July 2020).
Refactors the model structure criterion developed in Section 2 (plus 4.5 to 4.9) of The equivalence extension property and model structures
via the notion of cylindrical premodel category (called model setup
in the draft).
This makes it possible to state a sufficient and necessary criterion (Theorem 9.13) that is furthermore self-dual: a cylindrical premodel structure is a model structure exactly if:
The first condition can be restated as saying that trivial cofibrations are cogenerated by fibrations between fibration objects (e.g, universes in type theory), and dually for the second condition. They are vacuous in settings where all objects are cofibrant and fibrant (e.g., groupoids). Theoriginal criterion becomes a corollary (Theorem 10.5): every cylindrical premodel category with all objects cofibrant and the Frobenius and fibration extension is a proper model category (fibration extension gives cogeneration).
Constructive homotopy theory of marked semisimplicial sets (2018).
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 (2018).
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 (2017).
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) (2017), 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.
Generalized algebraic homotopy theories and applications (2023), inspired by recent work of Rafaël Bocquet.
Fibrancy of universes on the right (2023). Presents the ABCFHL proof of fibrancy of universes in a nice way.
Related: an older, much shorter note to the same effect for CCHM-style models (triggered by a question by Paolo Capriotti).
Evan Cavallo has found a way to unify the two cases.
An explanation of how to define higher cwfs in Segal types. Written for Thorsten Altenkirch in March 2020.
A synthetic argument (2020) that weakly filtered colimits commute with pullbacks (in spaces, but can be played out in any higher topos). This property fails in 1-categories, but in higher categorically pullbacks become a sound doctrine.
What the note calls weakly filtered
, I now like to call confluent
(a higher category is
See talk notes (Stockholm, 2020) for background. I needed a constructive argument for commutativity of finite limits and filtered colimits in higher toposes to attack the problem of showing constructively that the free higher group on a set has a set carrier.
Coalgebra models of type theory (2020). A categorical explanation of Pédrot internal presheaf model construction. Note that this model only interprets negative type formers (defined by something like a right universal property). For inductive type formers, one needs something more, such as the evil identity types used by Pédrot.
Semantics of signatures for higher inductive-inductive types (HIITs) in complete Segal types:
Colimit formulas for the n-truncation (for external n). Related: recursive formula for maps from n-truncation to (2n+2)-truncated type (for internal n).
Stuff on equivariant cubical model of HoTT.
Fibrancy of Π-types on the right (2019). Presents the ABCFHL proof of fibrancy of Π-types by reduction to trivial fibrations. Triggered by discussions with Awodey, Coquand, and Riehl at the Center for Advanced Study in Oslo during the special year on HoTT.
From fibrations in semisimplicial sets to uniform fibrations in symmetric simplicial sets (2019). Shows constructively that right Kan extension sends (trivial) Kan fibrations in semisimplicial sets between Kan fibrant objects with levelwise decidable equality to uniform (trivial) fibrations in (symmetric) simplicial sets. This can be used as gluing functor to obtain a constructive version of homotopy canonicity for homotopy type theory. However, it needs decidability of equality of elements in the initial model.
Simplicial colimits via cubical shapes (2018). This is well-known to homotopy theorists with much nicher proofs, but back then I did not know any of them and checked this for myself.
Some notes on directed univalence in bisimplicial sets (unfinished note, 2018). I think that the proof that F → 𝟚 × CovSpan is a Reedy fibration is broken. One should work around this by taking a Reedy fibrant replacement. Written for joint work with Cavallo and Riehl.
A categorical analysis of the fibrations of the cartesian model of cubical type theory.
Written in May 2018 in preparation for my talk at the Hausdorff Trimester Program Types, Sets and Constructions
to help me understand the new cartesian model.
Warning: contains lots of typos (e.g., first diagram do not mention ϕ).
Checks that the corresponding weak factorization system is still cofibrantly generated by a small set.
Normalization by evaluation for categories with families (unfinished note, early 2018). Contains the observation that the category of renamings Ren(C) may be defined abstractly as the initial cwf over C that is bijective on types.
Part of a sequence of abortive notes; the previous one was called twisted glue model (end of 2017), and much material did not make from paper.
During these months 2017–2018, I worked to present gluing and normalization by evaluation (via twisted gluing) cleanly in terms of cwfs. But I wanted to be categorically abstract (e.g., working with universal properties where possible) and avoid the bureaucracy of contexts and substitional stability (leading to duplication of work in presheaf-like setting). The abstraction rabbit hole lead only to starvation for me. (Now we have synthetic Tait computability by Jonathan Sterling.) If I were to try again, I would probably use universe categories as an intermediate tool.Thoughts on the gluing construction for categories with families (unfinished note, 2017). Contains an approach to the equivalence between categories with families and categories with attributes using comonadicity.
Joachim Kock's fat Δ, seen as a homotopical category, presents the homotopy theory of Δ (2017). That is, Δ_fat is a replacement Δ by a homotopical direct category.
Failure of algebraic universes for uniform fibrations in simplicial sets (2017).
Non-fibrancy of the interval in the CCHM cubical model (2015).
An examination of some potential generating categories of arrows for a constructive model of HoTT (2015).