2 citations · 2 across the 2 of their papers we have counts for
3 papers
cs.LO2022
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,…
cs.LO2021
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…
cs.LO2020★ 2 cited
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…