38 citations · 95 across the 13 of their papers we have counts for
16 papers
For the Metatheory of Type Theory, Internal Sconing Is Enough
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global…
Relative elegance and cartesian cubes with one connection
Evan Cavallo, Christian Sattler
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian…
Relative induction principles for type theories
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a func…
The effective model structure and -groupoid objects
Nicola Gambino, Simon Henry, Christian Sattler +1
For a category with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simpl…
Cubical models of -categories
Brandon Doherty, Chris Kapulkin, Zachery Lindsey +1
We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting…
Partial Univalence in n-truncated Type Theory
Christian Sattler, Andrea Vezzosi
It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial auto…
Constructive sheaf models of type theory
Thierry Coquand, Fabian Ruch, Christian Sattler
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive mo…
The constructive Kan-Quillen model structure: two new proofs
Nicola Gambino, Christian Sattler, Karol Szumiło
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs ar…
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
Andreas Abel, Christian Sattler
We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped w…
Canonicity and homotopy canonicity for cubical type theory
Thierry Coquand, Simon Huber, Christian Sattler
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained comput…
Constructive homotopy theory of marked semisimplicial sets
Christian Sattler
We develop the homotopy theory of semisimplicial sets constructively and without reference to point-set topology to obtain a constructive model for -groupoids. Most of the devel…
Idempotent completion of cubes in posets
Christian Sattler
This note concerns the category of cartesian cubes with connections, equivalently the full subcategory of posets on objects with . We show that the idempot…
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
Nicolai Kraus, Christian Sattler
Topologists are sometimes interested in space-valued diagrams over a given index category, but it is tricky to say what such a diagram even is if we look for a notion that is stabl…
The Equivalence Extension Property and Model Structures
Christian Sattler
We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spac…
The Frobenius Condition, Right Properness, and Uniform Fibrations
Nicola Gambino, Christian Sattler
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorizatio…
Higher Homotopies in a Hierarchy of Univalent Universes
Nicolai Kraus, Christian Sattler
For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a…