>>12728245If you understand how the types A * A and 2 -> A are isomorphic, then you understand how cubes work: they're functions from the interval type I to A.
The interval type is exactly like 2, but has a path constructor representing a line filling the space between the two points.
Then an equality p : x = y : A in MLTT is represented as
p' : I -> A
p' 0 = x : A
p' 1 = y : A
p' 2 = p : x = y : A
A square is the space enclosed between 4 points, or 2 lines, so it's 2 -> (2 -> A) == 2 * 2 ->A == 4 -> A, or I * I -> A, a function of two interval variables, and represents an equality between equalities u : p = q : x = y : A.
u' 0 0 = x
u' 0 1 = y
u' 0 2 = p
u' 1 0 = x
u' 1 1 = y
u' 1 2 = q
u' 2 2 = u
Notice how u 0 0 = u 1 0 and u 0 1 = u 1 1 doesn't have to be so and extrapolate from there.
