English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We study the conservativity of extensions by additional strict equalities ofdependent type theories (and more general second-order generalized algebraictheories). The conservativity of Extensional Type Theory over Intensional TypeTheory was proven by Hofmann. Our goal is to generalize such results to typetheories without the Uniqueness of Identity Proofs principles, such as variantsof Homotopy Type Theory.  For this purpose, we construct what is essentially the infinity-congruence onthe base theory that is freely generated by the considered equations. Thisinduces a factorization of any equational extension, whose two factors can bestudied independently. We conjecture that the first factor is always anequivalence when the base theory is well-behaved. We prove that the secondfactor is an equivalence when the infinity-congruence is 0-truncated.

Towards coherence theorems for equational extensions of type theories