Models of type theory with strict equality - Capriotti, Paolo (2017)
This thesis introduces the idea of two-level type theory, an extension of Martin-Löf type theory that adds a notion of strict equality as an internal primitive.