# Cubical Type

type theory## Part I.

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