{
"id": "1804.05045",
"version": "v1",
"published": "2018-04-13T17:22:19.000Z",
"updated": "2018-04-13T17:22:19.000Z",
"title": "Morita equivalences between algebraic dependent type theories",
"authors": [
"Valery Isaev"
],
"comment": "32 pages",
"categories": [
"math.CT",
"cs.LO",
"math.LO"
],
"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.",
"revisions": [
{
"version": "v1",
"updated": "2018-04-13T17:22:19.000Z"
}
],
"analyses": {
"keywords": [
"type theory",
"algebraic dependent type theories",
"morita equivalence",
"simple syntactic description",
"natural structure"
],
"note": {
"typesetting": "TeX",
"pages": 32,
"language": "en",
"license": "arXiv",
"status": "editable"
}
}
}