.. todo::
- minor gotcha: even if your particular flavor of hott is strongly
normalizing (so that all terms reduce to a unique normal form),
there are still types without decidable equality, because there
is no map inside type theory that computes normal forms of
arbitrary terms. find a way to say this without hopping back and
forth between meta-theoretical and internal statements.
you *would* obtain decidable equality from normalization if you
had equality reflection, but then you couldn't have strong
normalization, precisely because you'd get decidable equality.
.. todo::
decidable type checking
models
consequences of cubicaltt formalization