A cube with all faces being the same 2-loop.

puzzle.red

import path

let cube/2loop
  (A : type) (a : A)
  (sq : [i j] A [∂[i j] → a])
  : [i j k] A [
    | ∂[i] → sq j k
    | ∂[j] → sq i k
    | ∂[k] → sq i j
    ]
  =
  λ i j k →
  let face0 (x m : dim) : A =
    comp 0 x a [∂[k] | m=0 → refl | m=1 x → sq x k]
  in
  let face1 (x m : dim) : A =
    comp 1 x a [∂[k] | m=0 → refl | m=1 x → sq x k]
  in
  comp 0 1 (sq i j) [
  | i=0 → face1 j
  | j=1 → face0 i
  | j=0 → face1 i
  | i=1 → face0 j
  | ∂[k] → refl
  ]