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