English

Morita equivalences between algebraic dependent type theories

Category Theory 2020-09-29 v2 Logic in Computer Science Logic

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.

Keywords

Cite

@article{arxiv.1804.05045,
  title  = {Morita equivalences between algebraic dependent type theories},
  author = {Valery Isaev},
  journal= {arXiv preprint arXiv:1804.05045},
  year   = {2020}
}

Comments

34 pages

R2 v1 2026-06-23T01:23:12.292Z