2018/04/13 by Isaev, Valery · 1 citation
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1804.05045
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.