Valery Isaev: Morita equivalence between homotopy type theories.

Dependent type theories have many different constructions (such as sigma, pi, inductive types, universes, and so on). We describe a general notion of dependent type theory such that each of these individual constructions gives an example of such theory. These theories are organized into a category, so we can compare them and since this category is cocomplete, we can combine individual theories to obtain theories with several constructions. Finally, we consider theories with intensional identity types (which we might call homotopy type theories). Then it is natural to consider a notion of weak equivalence between such theories which we call Morita equivalence. Often we have two theories such that some rule holds in one of them judgementally and in the other one only propositionally. Then these theories are not isomorphic, but still can be Morita equivalent.