- Giving computational meaning to homotopy type theory.
- Martin-Loff uses concepts from topology
The most intuitie way to look at the interval type is [0,1]. It uses a morgan algebra, which is different from boolean, because i $\vee \neg i\neq true$.

You can make proves using paths. 

Pointwise equal functions are easy. This is not easy to prove in standard agd, but can be easily proven in cubical agda.