Let me then come to the last of the three questions. What is UTT
(univalent type theory)? As I conceive it:

It is any Martin-Lof type theory that is compatible with the idea
that equality/equivalence, as rendered by the identity type, is,
in general, structure rather than merely a property.

I find this definition somewhat puzzling. Cubicaltt is certainly compatible with the idea that equality is equivalence. But its path type seems to be a very different concept compared to Martin-Lof identity type.

What is a Martin-Lof type theory anyway? Are type systems based on untyped conversion (eg. Coq) Martin-Lof type theories? Are type theories with a different notion of equality (eg. observational or cubical type theories) also Martin-Lof type theories?

Andrew