Cubical Typetype theory
- What is cubical type theory?
It is a type theory giving homotopy type theory its computational meaning.
- What is homotopy type theory then?
It is traditional type theory (which refers to Martin-Löf type theory in this context) augmented with higher inductive types and the univalence axiom.
- So what are HIT and UA?
A HIT is a type equipped with custom equality. As an example, you can write a type similar to the natural numbers but with some equality between all even numbers. Well, it cannot be called natural numbers then.
- And UA?
It gives the universe the strongest possible equality in advance, because we do not define another universe.
To be continued…