6 papers
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…
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…
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…
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…