2 citations · 5 across the 6 of their papers we have counts for
7 papers
Strict Rezk completions of models of HoTT and homotopy canonicity
Rafaël Bocquet
We give a new constructive proof of homotopy canonicity for homotopy type theory (HoTT). Canonicity proofs typically involve gluing constructions over the syntax of type theory. We…
Towards coherence theorems for equational extensions of type theories
Rafaël Bocquet
We study the conservativity of extensions by additional strict equalities of dependent type theories (and more general second-order generalized algebraic theories). The conservativ…
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…
External univalence for second-order generalized algebraic theories
Rafaël Bocquet
Voevodsky's univalence axiom is often motivated as a realization of the equivalence principle; the idea that equivalent mathematical structures satisfy the same properties. Indeed,…
Strictification of weakly stable type-theoretic structures using generic contexts
Rafaël Bocquet
We present a new strictification method for type-theoretic structures that are only weakly stable under substitution. Given weakly stable structures over some model of type theory,…
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…
Coherence of strict equalities in dependent type theories
Rafaël Bocquet
We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of…