In recent years a number of extensions of Martin-Löf type theory (MLTT) [1]} have been proposed to
enhance the expressiveness or usability of the type theory. The most famous of these is Homotopy Type Theory [2]},
but other directions include the related Cubical Type Theory [3]},
FreshMLTT [4]}, a type theory with name abstraction
based on nominal sets, and Type Theory in Color [5]}
for internalising relational parametricity in type theory. Many
of these extensions use denotational semantics to argue for consistency and to inspire constructions in the language.
