38 citations · 95 across the 13 of their papers we have counts for
3 papers · 1 filter
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 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…