An Ad-Hoc Semantics to Study Structural Properties of Types

The paper illustrates a sound and complete semantics with a classifying model for Martin-Löf type theory, which can be easily extended to a large fragment of homotopy type theory (HoTT). The semantics is ad-hoc in the sense that it is not intended to provide a meaning to the system, but to study its proof-theoretical properties using the classifying model, allowing to derive that Π is injective, and no universe is equivalent to a function space, in analogy with the PER models by Abel, Coquand, and Dybjer, but including an infinite hierarchy of universes.