Proof theory
============

Normalization
-------------

.. 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