Morita equivalences between algebraic dependent type theories

arXiv1804.05045MaRDI QIDQ6300330FDOQ6300330

Publication date: 13 April 2018

Abstract: 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.

This page was built for publication: Morita equivalences between algebraic dependent type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6300330)