Cubical Type

Part I.

1. What is cubical type theory?

It is a type theory giving homotopy type theory its computational meaning.

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

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

4. And UA?

It gives the universe the strongest possible equality in advance, because we do not define another universe.

To be continued…