Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1)
               (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U
  = PathP (<i> (Path A (u @ i) (v @ i))) r0 r1

-- Exercise construct a constant square:
constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p =
  <i k> comp (<j> A) a [
    (i = 0) -> <j> p @ -j \/ k,
    (i = 1) -> <j> p @ j /\ k,
    (k = 0) -> <j> p @ i \/ -j,
    (k = 1) -> <j> p @ i /\ j
  ]