arXiv Analytics

Sign in

arXiv:1804.05045 [math.CT]AbstractReferencesReviewsResources

Morita equivalences between algebraic dependent type theories

Valery Isaev

Published 2018-04-13Version 1

We define a notion of equivalence between algebraic dependent type theories which we call Morita equivalence. This notion has a simple syntactic description and an equivalent description in terms of models of the theories. The category of models of a type theory often carries a natural structure of a model category. If this holds for the categories of models of two theories, then a map between them is a Morita equivalence if and only if the adjunction generated by it is a Quillen equivalence.

Comments: 32 pages
Categories: math.CT, cs.LO, math.LO
Related articles: Most relevant | Search more
arXiv:1705.07442 [math.CT] (Published 2017-05-21)
A type theory for synthetic $\infty$-categories
arXiv:2105.00283 [math.CT] (Published 2021-05-01)
Dialectica models of type theory
arXiv:2205.10917 [math.CT] (Published 2022-05-22)
On Hofmann-Streicher universes

Links

Toolbox