comp on a 6-cube with iterated path types, takes at least an hour to type check.

comp6iterated.red

def pathd (A : 𝕀 → type) (M : A 0) (N : A 1) : type =
  [i] A i [
  | i=0 → M
  | i=1 → N
  ]

def path (A : type) (M N : A) : type =
  [i] A [
  | i=0 → M
  | i=1 → N
  ]

def comp6Cube (A : type) (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : A)
  (a0000i : path A a0 a1)
  (a0001i : path A a2 a3)
  (a000i0 : path A a0 a2)
  (a000i1 : path A a1 a3)
  (a0010i : path A a4 a5)
  (a0011i : path A a6 a7)
  (a001i0 : path A a4 a6)
  (a001i1 : path A a5 a7)
  (a00i00 : path A a0 a4)
  (a00i01 : path A a1 a5)
  (a00i10 : path A a2 a6)
  (a00i11 : path A a3 a7)
  (a0100i : path A a8 a9)
  (a0101i : path A a10 a11)
  (a010i0 : path A a8 a10)
  (a010i1 : path A a9 a11)
  (a0110i : path A a12 a13)
  (a0111i : path A a14 a15)
  (a011i0 : path A a12 a14)
  (a011i1 : path A a13 a15)
  (a01i00 : path A a8 a12)
  (a01i01 : path A a9 a13)
  (a01i10 : path A a10 a14)
  (a01i11 : path A a11 a15)
  (a0i000 : path A a0 a8)
  (a0i001 : path A a1 a9)
  (a0i010 : path A a2 a10)
  (a0i011 : path A a3 a11)
  (a0i100 : path A a4 a12)
  (a0i101 : path A a5 a13)
  (a0i110 : path A a6 a14)
  (a0i111 : path A a7 a15)
  (a1000i : path A a16 a17)
  (a1001i : path A a18 a19)
  (a100i0 : path A a16 a18)
  (a100i1 : path A a17 a19)
  (a1010i : path A a20 a21)
  (a1011i : path A a22 a23)
  (a101i0 : path A a20 a22)
  (a101i1 : path A a21 a23)
  (a10i00 : path A a16 a20)
  (a10i01 : path A a17 a21)
  (a10i10 : path A a18 a22)
  (a10i11 : path A a19 a23)
  (a1100i : path A a24 a25)
  (a1101i : path A a26 a27)
  (a110i0 : path A a24 a26)
  (a110i1 : path A a25 a27)
  (a1110i : path A a28 a29)
  (a1111i : path A a30 a31)
  (a111i0 : path A a28 a30)
  (a111i1 : path A a29 a31)
  (a11i00 : path A a24 a28)
  (a11i01 : path A a25 a29)
  (a11i10 : path A a26 a30)
  (a11i11 : path A a27 a31)
  (a1i000 : path A a16 a24)
  (a1i001 : path A a17 a25)
  (a1i010 : path A a18 a26)
  (a1i011 : path A a19 a27)
  (a1i100 : path A a20 a28)
  (a1i101 : path A a21 a29)
  (a1i110 : path A a22 a30)
  (a1i111 : path A a23 a31)
  (ai0000 : path A a0 a16)
  (ai0001 : path A a1 a17)
  (ai0010 : path A a2 a18)
  (ai0011 : path A a3 a19)
  (ai0100 : path A a4 a20)
  (ai0101 : path A a5 a21)
  (ai0110 : path A a6 a22)
  (ai0111 : path A a7 a23)
  (ai1000 : path A a8 a24)
  (ai1001 : path A a9 a25)
  (ai1010 : path A a10 a26)
  (ai1011 : path A a11 a27)
  (ai1100 : path A a12 a28)
  (ai1101 : path A a13 a29)
  (ai1110 : path A a14 a30)
  (ai1111 : path A a15 a31)
  (b0000i : path A b0 b1)
  (b0001i : path A b2 b3)
  (b000i0 : path A b0 b2)
  (b000i1 : path A b1 b3)
  (b0010i : path A b4 b5)
  (b0011i : path A b6 b7)
  (b001i0 : path A b4 b6)
  (b001i1 : path A b5 b7)
  (b00i00 : path A b0 b4)
  (b00i01 : path A b1 b5)
  (b00i10 : path A b2 b6)
  (b00i11 : path A b3 b7)
  (b0100i : path A b8 b9)
  (b0101i : path A b10 b11)
  (b010i0 : path A b8 b10)
  (b010i1 : path A b9 b11)
  (b0110i : path A b12 b13)
  (b0111i : path A b14 b15)
  (b011i0 : path A b12 b14)
  (b011i1 : path A b13 b15)
  (b01i00 : path A b8 b12)
  (b01i01 : path A b9 b13)
  (b01i10 : path A b10 b14)
  (b01i11 : path A b11 b15)
  (b0i000 : path A b0 b8)
  (b0i001 : path A b1 b9)
  (b0i010 : path A b2 b10)
  (b0i011 : path A b3 b11)
  (b0i100 : path A b4 b12)
  (b0i101 : path A b5 b13)
  (b0i110 : path A b6 b14)
  (b0i111 : path A b7 b15)
  (b1000i : path A b16 b17)
  (b1001i : path A b18 b19)
  (b100i0 : path A b16 b18)
  (b100i1 : path A b17 b19)
  (b1010i : path A b20 b21)
  (b1011i : path A b22 b23)
  (b101i0 : path A b20 b22)
  (b101i1 : path A b21 b23)
  (b10i00 : path A b16 b20)
  (b10i01 : path A b17 b21)
  (b10i10 : path A b18 b22)
  (b10i11 : path A b19 b23)
  (b1100i : path A b24 b25)
  (b1101i : path A b26 b27)
  (b110i0 : path A b24 b26)
  (b110i1 : path A b25 b27)
  (b1110i : path A b28 b29)
  (b1111i : path A b30 b31)
  (b111i0 : path A b28 b30)
  (b111i1 : path A b29 b31)
  (b11i00 : path A b24 b28)
  (b11i01 : path A b25 b29)
  (b11i10 : path A b26 b30)
  (b11i11 : path A b27 b31)
  (b1i000 : path A b16 b24)
  (b1i001 : path A b17 b25)
  (b1i010 : path A b18 b26)
  (b1i011 : path A b19 b27)
  (b1i100 : path A b20 b28)
  (b1i101 : path A b21 b29)
  (b1i110 : path A b22 b30)
  (b1i111 : path A b23 b31)
  (bi0000 : path A b0 b16)
  (bi0001 : path A b1 b17)
  (bi0010 : path A b2 b18)
  (bi0011 : path A b3 b19)
  (bi0100 : path A b4 b20)
  (bi0101 : path A b5 b21)
  (bi0110 : path A b6 b22)
  (bi0111 : path A b7 b23)
  (bi1000 : path A b8 b24)
  (bi1001 : path A b9 b25)
  (bi1010 : path A b10 b26)
  (bi1011 : path A b11 b27)
  (bi1100 : path A b12 b28)
  (bi1101 : path A b13 b29)
  (bi1110 : path A b14 b30)
  (bi1111 : path A b15 b31)
  (k00000 : path A a0 b0)
  (k00001 : path A a1 b1)
  (k00010 : path A a2 b2)
  (k00011 : path A a3 b3)
  (k00100 : path A a4 b4)
  (k00101 : path A a5 b5)
  (k00110 : path A a6 b6)
  (k00111 : path A a7 b7)
  (k01000 : path A a8 b8)
  (k01001 : path A a9 b9)
  (k01010 : path A a10 b10)
  (k01011 : path A a11 b11)
  (k01100 : path A a12 b12)
  (k01101 : path A a13 b13)
  (k01110 : path A a14 b14)
  (k01111 : path A a15 b15)
  (k10000 : path A a16 b16)
  (k10001 : path A a17 b17)
  (k10010 : path A a18 b18)
  (k10011 : path A a19 b19)
  (k10100 : path A a20 b20)
  (k10101 : path A a21 b21)
  (k10110 : path A a22 b22)
  (k10111 : path A a23 b23)
  (k11000 : path A a24 b24)
  (k11001 : path A a25 b25)
  (k11010 : path A a26 b26)
  (k11011 : path A a27 b27)
  (k11100 : path A a28 b28)
  (k11101 : path A a29 b29)
  (k11110 : path A a30 b30)
  (k11111 : path A a31 b31)
  (a000ii : pathd (λ j0 → path A (a0000i j0) (a0001i j0)) a000i0 a000i1)
  (a001ii : pathd (λ j0 → path A (a0010i j0) (a0011i j0)) a001i0 a001i1)
  (a00i0i : pathd (λ j0 → path A (a0000i j0) (a0010i j0)) a00i00 a00i01)
  (a00i1i : pathd (λ j0 → path A (a0001i j0) (a0011i j0)) a00i10 a00i11)
  (a00ii0 : pathd (λ j0 → path A (a000i0 j0) (a001i0 j0)) a00i00 a00i10)
  (a00ii1 : pathd (λ j0 → path A (a000i1 j0) (a001i1 j0)) a00i01 a00i11)
  (a010ii : pathd (λ j0 → path A (a0100i j0) (a0101i j0)) a010i0 a010i1)
  (a011ii : pathd (λ j0 → path A (a0110i j0) (a0111i j0)) a011i0 a011i1)
  (a01i0i : pathd (λ j0 → path A (a0100i j0) (a0110i j0)) a01i00 a01i01)
  (a01i1i : pathd (λ j0 → path A (a0101i j0) (a0111i j0)) a01i10 a01i11)
  (a01ii0 : pathd (λ j0 → path A (a010i0 j0) (a011i0 j0)) a01i00 a01i10)
  (a01ii1 : pathd (λ j0 → path A (a010i1 j0) (a011i1 j0)) a01i01 a01i11)
  (a0i00i : pathd (λ j0 → path A (a0000i j0) (a0100i j0)) a0i000 a0i001)
  (a0i01i : pathd (λ j0 → path A (a0001i j0) (a0101i j0)) a0i010 a0i011)
  (a0i0i0 : pathd (λ j0 → path A (a000i0 j0) (a010i0 j0)) a0i000 a0i010)
  (a0i0i1 : pathd (λ j0 → path A (a000i1 j0) (a010i1 j0)) a0i001 a0i011)
  (a0i10i : pathd (λ j0 → path A (a0010i j0) (a0110i j0)) a0i100 a0i101)
  (a0i11i : pathd (λ j0 → path A (a0011i j0) (a0111i j0)) a0i110 a0i111)
  (a0i1i0 : pathd (λ j0 → path A (a001i0 j0) (a011i0 j0)) a0i100 a0i110)
  (a0i1i1 : pathd (λ j0 → path A (a001i1 j0) (a011i1 j0)) a0i101 a0i111)
  (a0ii00 : pathd (λ j0 → path A (a00i00 j0) (a01i00 j0)) a0i000 a0i100)
  (a0ii01 : pathd (λ j0 → path A (a00i01 j0) (a01i01 j0)) a0i001 a0i101)
  (a0ii10 : pathd (λ j0 → path A (a00i10 j0) (a01i10 j0)) a0i010 a0i110)
  (a0ii11 : pathd (λ j0 → path A (a00i11 j0) (a01i11 j0)) a0i011 a0i111)
  (a100ii : pathd (λ j0 → path A (a1000i j0) (a1001i j0)) a100i0 a100i1)
  (a101ii : pathd (λ j0 → path A (a1010i j0) (a1011i j0)) a101i0 a101i1)
  (a10i0i : pathd (λ j0 → path A (a1000i j0) (a1010i j0)) a10i00 a10i01)
  (a10i1i : pathd (λ j0 → path A (a1001i j0) (a1011i j0)) a10i10 a10i11)
  (a10ii0 : pathd (λ j0 → path A (a100i0 j0) (a101i0 j0)) a10i00 a10i10)
  (a10ii1 : pathd (λ j0 → path A (a100i1 j0) (a101i1 j0)) a10i01 a10i11)
  (a110ii : pathd (λ j0 → path A (a1100i j0) (a1101i j0)) a110i0 a110i1)
  (a111ii : pathd (λ j0 → path A (a1110i j0) (a1111i j0)) a111i0 a111i1)
  (a11i0i : pathd (λ j0 → path A (a1100i j0) (a1110i j0)) a11i00 a11i01)
  (a11i1i : pathd (λ j0 → path A (a1101i j0) (a1111i j0)) a11i10 a11i11)
  (a11ii0 : pathd (λ j0 → path A (a110i0 j0) (a111i0 j0)) a11i00 a11i10)
  (a11ii1 : pathd (λ j0 → path A (a110i1 j0) (a111i1 j0)) a11i01 a11i11)
  (a1i00i : pathd (λ j0 → path A (a1000i j0) (a1100i j0)) a1i000 a1i001)
  (a1i01i : pathd (λ j0 → path A (a1001i j0) (a1101i j0)) a1i010 a1i011)
  (a1i0i0 : pathd (λ j0 → path A (a100i0 j0) (a110i0 j0)) a1i000 a1i010)
  (a1i0i1 : pathd (λ j0 → path A (a100i1 j0) (a110i1 j0)) a1i001 a1i011)
  (a1i10i : pathd (λ j0 → path A (a1010i j0) (a1110i j0)) a1i100 a1i101)
  (a1i11i : pathd (λ j0 → path A (a1011i j0) (a1111i j0)) a1i110 a1i111)
  (a1i1i0 : pathd (λ j0 → path A (a101i0 j0) (a111i0 j0)) a1i100 a1i110)
  (a1i1i1 : pathd (λ j0 → path A (a101i1 j0) (a111i1 j0)) a1i101 a1i111)
  (a1ii00 : pathd (λ j0 → path A (a10i00 j0) (a11i00 j0)) a1i000 a1i100)
  (a1ii01 : pathd (λ j0 → path A (a10i01 j0) (a11i01 j0)) a1i001 a1i101)
  (a1ii10 : pathd (λ j0 → path A (a10i10 j0) (a11i10 j0)) a1i010 a1i110)
  (a1ii11 : pathd (λ j0 → path A (a10i11 j0) (a11i11 j0)) a1i011 a1i111)
  (ai000i : pathd (λ j0 → path A (a0000i j0) (a1000i j0)) ai0000 ai0001)
  (ai001i : pathd (λ j0 → path A (a0001i j0) (a1001i j0)) ai0010 ai0011)
  (ai00i0 : pathd (λ j0 → path A (a000i0 j0) (a100i0 j0)) ai0000 ai0010)
  (ai00i1 : pathd (λ j0 → path A (a000i1 j0) (a100i1 j0)) ai0001 ai0011)
  (ai010i : pathd (λ j0 → path A (a0010i j0) (a1010i j0)) ai0100 ai0101)
  (ai011i : pathd (λ j0 → path A (a0011i j0) (a1011i j0)) ai0110 ai0111)
  (ai01i0 : pathd (λ j0 → path A (a001i0 j0) (a101i0 j0)) ai0100 ai0110)
  (ai01i1 : pathd (λ j0 → path A (a001i1 j0) (a101i1 j0)) ai0101 ai0111)
  (ai0i00 : pathd (λ j0 → path A (a00i00 j0) (a10i00 j0)) ai0000 ai0100)
  (ai0i01 : pathd (λ j0 → path A (a00i01 j0) (a10i01 j0)) ai0001 ai0101)
  (ai0i10 : pathd (λ j0 → path A (a00i10 j0) (a10i10 j0)) ai0010 ai0110)
  (ai0i11 : pathd (λ j0 → path A (a00i11 j0) (a10i11 j0)) ai0011 ai0111)
  (ai100i : pathd (λ j0 → path A (a0100i j0) (a1100i j0)) ai1000 ai1001)
  (ai101i : pathd (λ j0 → path A (a0101i j0) (a1101i j0)) ai1010 ai1011)
  (ai10i0 : pathd (λ j0 → path A (a010i0 j0) (a110i0 j0)) ai1000 ai1010)
  (ai10i1 : pathd (λ j0 → path A (a010i1 j0) (a110i1 j0)) ai1001 ai1011)
  (ai110i : pathd (λ j0 → path A (a0110i j0) (a1110i j0)) ai1100 ai1101)
  (ai111i : pathd (λ j0 → path A (a0111i j0) (a1111i j0)) ai1110 ai1111)
  (ai11i0 : pathd (λ j0 → path A (a011i0 j0) (a111i0 j0)) ai1100 ai1110)
  (ai11i1 : pathd (λ j0 → path A (a011i1 j0) (a111i1 j0)) ai1101 ai1111)
  (ai1i00 : pathd (λ j0 → path A (a01i00 j0) (a11i00 j0)) ai1000 ai1100)
  (ai1i01 : pathd (λ j0 → path A (a01i01 j0) (a11i01 j0)) ai1001 ai1101)
  (ai1i10 : pathd (λ j0 → path A (a01i10 j0) (a11i10 j0)) ai1010 ai1110)
  (ai1i11 : pathd (λ j0 → path A (a01i11 j0) (a11i11 j0)) ai1011 ai1111)
  (aii000 : pathd (λ j0 → path A (a0i000 j0) (a1i000 j0)) ai0000 ai1000)
  (aii001 : pathd (λ j0 → path A (a0i001 j0) (a1i001 j0)) ai0001 ai1001)
  (aii010 : pathd (λ j0 → path A (a0i010 j0) (a1i010 j0)) ai0010 ai1010)
  (aii011 : pathd (λ j0 → path A (a0i011 j0) (a1i011 j0)) ai0011 ai1011)
  (aii100 : pathd (λ j0 → path A (a0i100 j0) (a1i100 j0)) ai0100 ai1100)
  (aii101 : pathd (λ j0 → path A (a0i101 j0) (a1i101 j0)) ai0101 ai1101)
  (aii110 : pathd (λ j0 → path A (a0i110 j0) (a1i110 j0)) ai0110 ai1110)
  (aii111 : pathd (λ j0 → path A (a0i111 j0) (a1i111 j0)) ai0111 ai1111)
  (b000ii : pathd (λ j0 → path A (b0000i j0) (b0001i j0)) b000i0 b000i1)
  (b001ii : pathd (λ j0 → path A (b0010i j0) (b0011i j0)) b001i0 b001i1)
  (b00i0i : pathd (λ j0 → path A (b0000i j0) (b0010i j0)) b00i00 b00i01)
  (b00i1i : pathd (λ j0 → path A (b0001i j0) (b0011i j0)) b00i10 b00i11)
  (b00ii0 : pathd (λ j0 → path A (b000i0 j0) (b001i0 j0)) b00i00 b00i10)
  (b00ii1 : pathd (λ j0 → path A (b000i1 j0) (b001i1 j0)) b00i01 b00i11)
  (b010ii : pathd (λ j0 → path A (b0100i j0) (b0101i j0)) b010i0 b010i1)
  (b011ii : pathd (λ j0 → path A (b0110i j0) (b0111i j0)) b011i0 b011i1)
  (b01i0i : pathd (λ j0 → path A (b0100i j0) (b0110i j0)) b01i00 b01i01)
  (b01i1i : pathd (λ j0 → path A (b0101i j0) (b0111i j0)) b01i10 b01i11)
  (b01ii0 : pathd (λ j0 → path A (b010i0 j0) (b011i0 j0)) b01i00 b01i10)
  (b01ii1 : pathd (λ j0 → path A (b010i1 j0) (b011i1 j0)) b01i01 b01i11)
  (b0i00i : pathd (λ j0 → path A (b0000i j0) (b0100i j0)) b0i000 b0i001)
  (b0i01i : pathd (λ j0 → path A (b0001i j0) (b0101i j0)) b0i010 b0i011)
  (b0i0i0 : pathd (λ j0 → path A (b000i0 j0) (b010i0 j0)) b0i000 b0i010)
  (b0i0i1 : pathd (λ j0 → path A (b000i1 j0) (b010i1 j0)) b0i001 b0i011)
  (b0i10i : pathd (λ j0 → path A (b0010i j0) (b0110i j0)) b0i100 b0i101)
  (b0i11i : pathd (λ j0 → path A (b0011i j0) (b0111i j0)) b0i110 b0i111)
  (b0i1i0 : pathd (λ j0 → path A (b001i0 j0) (b011i0 j0)) b0i100 b0i110)
  (b0i1i1 : pathd (λ j0 → path A (b001i1 j0) (b011i1 j0)) b0i101 b0i111)
  (b0ii00 : pathd (λ j0 → path A (b00i00 j0) (b01i00 j0)) b0i000 b0i100)
  (b0ii01 : pathd (λ j0 → path A (b00i01 j0) (b01i01 j0)) b0i001 b0i101)
  (b0ii10 : pathd (λ j0 → path A (b00i10 j0) (b01i10 j0)) b0i010 b0i110)
  (b0ii11 : pathd (λ j0 → path A (b00i11 j0) (b01i11 j0)) b0i011 b0i111)
  (b100ii : pathd (λ j0 → path A (b1000i j0) (b1001i j0)) b100i0 b100i1)
  (b101ii : pathd (λ j0 → path A (b1010i j0) (b1011i j0)) b101i0 b101i1)
  (b10i0i : pathd (λ j0 → path A (b1000i j0) (b1010i j0)) b10i00 b10i01)
  (b10i1i : pathd (λ j0 → path A (b1001i j0) (b1011i j0)) b10i10 b10i11)
  (b10ii0 : pathd (λ j0 → path A (b100i0 j0) (b101i0 j0)) b10i00 b10i10)
  (b10ii1 : pathd (λ j0 → path A (b100i1 j0) (b101i1 j0)) b10i01 b10i11)
  (b110ii : pathd (λ j0 → path A (b1100i j0) (b1101i j0)) b110i0 b110i1)
  (b111ii : pathd (λ j0 → path A (b1110i j0) (b1111i j0)) b111i0 b111i1)
  (b11i0i : pathd (λ j0 → path A (b1100i j0) (b1110i j0)) b11i00 b11i01)
  (b11i1i : pathd (λ j0 → path A (b1101i j0) (b1111i j0)) b11i10 b11i11)
  (b11ii0 : pathd (λ j0 → path A (b110i0 j0) (b111i0 j0)) b11i00 b11i10)
  (b11ii1 : pathd (λ j0 → path A (b110i1 j0) (b111i1 j0)) b11i01 b11i11)
  (b1i00i : pathd (λ j0 → path A (b1000i j0) (b1100i j0)) b1i000 b1i001)
  (b1i01i : pathd (λ j0 → path A (b1001i j0) (b1101i j0)) b1i010 b1i011)
  (b1i0i0 : pathd (λ j0 → path A (b100i0 j0) (b110i0 j0)) b1i000 b1i010)
  (b1i0i1 : pathd (λ j0 → path A (b100i1 j0) (b110i1 j0)) b1i001 b1i011)
  (b1i10i : pathd (λ j0 → path A (b1010i j0) (b1110i j0)) b1i100 b1i101)
  (b1i11i : pathd (λ j0 → path A (b1011i j0) (b1111i j0)) b1i110 b1i111)
  (b1i1i0 : pathd (λ j0 → path A (b101i0 j0) (b111i0 j0)) b1i100 b1i110)
  (b1i1i1 : pathd (λ j0 → path A (b101i1 j0) (b111i1 j0)) b1i101 b1i111)
  (b1ii00 : pathd (λ j0 → path A (b10i00 j0) (b11i00 j0)) b1i000 b1i100)
  (b1ii01 : pathd (λ j0 → path A (b10i01 j0) (b11i01 j0)) b1i001 b1i101)
  (b1ii10 : pathd (λ j0 → path A (b10i10 j0) (b11i10 j0)) b1i010 b1i110)
  (b1ii11 : pathd (λ j0 → path A (b10i11 j0) (b11i11 j0)) b1i011 b1i111)
  (bi000i : pathd (λ j0 → path A (b0000i j0) (b1000i j0)) bi0000 bi0001)
  (bi001i : pathd (λ j0 → path A (b0001i j0) (b1001i j0)) bi0010 bi0011)
  (bi00i0 : pathd (λ j0 → path A (b000i0 j0) (b100i0 j0)) bi0000 bi0010)
  (bi00i1 : pathd (λ j0 → path A (b000i1 j0) (b100i1 j0)) bi0001 bi0011)
  (bi010i : pathd (λ j0 → path A (b0010i j0) (b1010i j0)) bi0100 bi0101)
  (bi011i : pathd (λ j0 → path A (b0011i j0) (b1011i j0)) bi0110 bi0111)
  (bi01i0 : pathd (λ j0 → path A (b001i0 j0) (b101i0 j0)) bi0100 bi0110)
  (bi01i1 : pathd (λ j0 → path A (b001i1 j0) (b101i1 j0)) bi0101 bi0111)
  (bi0i00 : pathd (λ j0 → path A (b00i00 j0) (b10i00 j0)) bi0000 bi0100)
  (bi0i01 : pathd (λ j0 → path A (b00i01 j0) (b10i01 j0)) bi0001 bi0101)
  (bi0i10 : pathd (λ j0 → path A (b00i10 j0) (b10i10 j0)) bi0010 bi0110)
  (bi0i11 : pathd (λ j0 → path A (b00i11 j0) (b10i11 j0)) bi0011 bi0111)
  (bi100i : pathd (λ j0 → path A (b0100i j0) (b1100i j0)) bi1000 bi1001)
  (bi101i : pathd (λ j0 → path A (b0101i j0) (b1101i j0)) bi1010 bi1011)
  (bi10i0 : pathd (λ j0 → path A (b010i0 j0) (b110i0 j0)) bi1000 bi1010)
  (bi10i1 : pathd (λ j0 → path A (b010i1 j0) (b110i1 j0)) bi1001 bi1011)
  (bi110i : pathd (λ j0 → path A (b0110i j0) (b1110i j0)) bi1100 bi1101)
  (bi111i : pathd (λ j0 → path A (b0111i j0) (b1111i j0)) bi1110 bi1111)
  (bi11i0 : pathd (λ j0 → path A (b011i0 j0) (b111i0 j0)) bi1100 bi1110)
  (bi11i1 : pathd (λ j0 → path A (b011i1 j0) (b111i1 j0)) bi1101 bi1111)
  (bi1i00 : pathd (λ j0 → path A (b01i00 j0) (b11i00 j0)) bi1000 bi1100)
  (bi1i01 : pathd (λ j0 → path A (b01i01 j0) (b11i01 j0)) bi1001 bi1101)
  (bi1i10 : pathd (λ j0 → path A (b01i10 j0) (b11i10 j0)) bi1010 bi1110)
  (bi1i11 : pathd (λ j0 → path A (b01i11 j0) (b11i11 j0)) bi1011 bi1111)
  (bii000 : pathd (λ j0 → path A (b0i000 j0) (b1i000 j0)) bi0000 bi1000)
  (bii001 : pathd (λ j0 → path A (b0i001 j0) (b1i001 j0)) bi0001 bi1001)
  (bii010 : pathd (λ j0 → path A (b0i010 j0) (b1i010 j0)) bi0010 bi1010)
  (bii011 : pathd (λ j0 → path A (b0i011 j0) (b1i011 j0)) bi0011 bi1011)
  (bii100 : pathd (λ j0 → path A (b0i100 j0) (b1i100 j0)) bi0100 bi1100)
  (bii101 : pathd (λ j0 → path A (b0i101 j0) (b1i101 j0)) bi0101 bi1101)
  (bii110 : pathd (λ j0 → path A (b0i110 j0) (b1i110 j0)) bi0110 bi1110)
  (bii111 : pathd (λ j0 → path A (b0i111 j0) (b1i111 j0)) bi0111 bi1111)
  (k0000i : pathd (λ j0 → path A (a0000i j0) (b0000i j0)) k00000 k00001)
  (k0001i : pathd (λ j0 → path A (a0001i j0) (b0001i j0)) k00010 k00011)
  (k000i0 : pathd (λ j0 → path A (a000i0 j0) (b000i0 j0)) k00000 k00010)
  (k000i1 : pathd (λ j0 → path A (a000i1 j0) (b000i1 j0)) k00001 k00011)
  (k0010i : pathd (λ j0 → path A (a0010i j0) (b0010i j0)) k00100 k00101)
  (k0011i : pathd (λ j0 → path A (a0011i j0) (b0011i j0)) k00110 k00111)
  (k001i0 : pathd (λ j0 → path A (a001i0 j0) (b001i0 j0)) k00100 k00110)
  (k001i1 : pathd (λ j0 → path A (a001i1 j0) (b001i1 j0)) k00101 k00111)
  (k00i00 : pathd (λ j0 → path A (a00i00 j0) (b00i00 j0)) k00000 k00100)
  (k00i01 : pathd (λ j0 → path A (a00i01 j0) (b00i01 j0)) k00001 k00101)
  (k00i10 : pathd (λ j0 → path A (a00i10 j0) (b00i10 j0)) k00010 k00110)
  (k00i11 : pathd (λ j0 → path A (a00i11 j0) (b00i11 j0)) k00011 k00111)
  (k0100i : pathd (λ j0 → path A (a0100i j0) (b0100i j0)) k01000 k01001)
  (k0101i : pathd (λ j0 → path A (a0101i j0) (b0101i j0)) k01010 k01011)
  (k010i0 : pathd (λ j0 → path A (a010i0 j0) (b010i0 j0)) k01000 k01010)
  (k010i1 : pathd (λ j0 → path A (a010i1 j0) (b010i1 j0)) k01001 k01011)
  (k0110i : pathd (λ j0 → path A (a0110i j0) (b0110i j0)) k01100 k01101)
  (k0111i : pathd (λ j0 → path A (a0111i j0) (b0111i j0)) k01110 k01111)
  (k011i0 : pathd (λ j0 → path A (a011i0 j0) (b011i0 j0)) k01100 k01110)
  (k011i1 : pathd (λ j0 → path A (a011i1 j0) (b011i1 j0)) k01101 k01111)
  (k01i00 : pathd (λ j0 → path A (a01i00 j0) (b01i00 j0)) k01000 k01100)
  (k01i01 : pathd (λ j0 → path A (a01i01 j0) (b01i01 j0)) k01001 k01101)
  (k01i10 : pathd (λ j0 → path A (a01i10 j0) (b01i10 j0)) k01010 k01110)
  (k01i11 : pathd (λ j0 → path A (a01i11 j0) (b01i11 j0)) k01011 k01111)
  (k0i000 : pathd (λ j0 → path A (a0i000 j0) (b0i000 j0)) k00000 k01000)
  (k0i001 : pathd (λ j0 → path A (a0i001 j0) (b0i001 j0)) k00001 k01001)
  (k0i010 : pathd (λ j0 → path A (a0i010 j0) (b0i010 j0)) k00010 k01010)
  (k0i011 : pathd (λ j0 → path A (a0i011 j0) (b0i011 j0)) k00011 k01011)
  (k0i100 : pathd (λ j0 → path A (a0i100 j0) (b0i100 j0)) k00100 k01100)
  (k0i101 : pathd (λ j0 → path A (a0i101 j0) (b0i101 j0)) k00101 k01101)
  (k0i110 : pathd (λ j0 → path A (a0i110 j0) (b0i110 j0)) k00110 k01110)
  (k0i111 : pathd (λ j0 → path A (a0i111 j0) (b0i111 j0)) k00111 k01111)
  (k1000i : pathd (λ j0 → path A (a1000i j0) (b1000i j0)) k10000 k10001)
  (k1001i : pathd (λ j0 → path A (a1001i j0) (b1001i j0)) k10010 k10011)
  (k100i0 : pathd (λ j0 → path A (a100i0 j0) (b100i0 j0)) k10000 k10010)
  (k100i1 : pathd (λ j0 → path A (a100i1 j0) (b100i1 j0)) k10001 k10011)
  (k1010i : pathd (λ j0 → path A (a1010i j0) (b1010i j0)) k10100 k10101)
  (k1011i : pathd (λ j0 → path A (a1011i j0) (b1011i j0)) k10110 k10111)
  (k101i0 : pathd (λ j0 → path A (a101i0 j0) (b101i0 j0)) k10100 k10110)
  (k101i1 : pathd (λ j0 → path A (a101i1 j0) (b101i1 j0)) k10101 k10111)
  (k10i00 : pathd (λ j0 → path A (a10i00 j0) (b10i00 j0)) k10000 k10100)
  (k10i01 : pathd (λ j0 → path A (a10i01 j0) (b10i01 j0)) k10001 k10101)
  (k10i10 : pathd (λ j0 → path A (a10i10 j0) (b10i10 j0)) k10010 k10110)
  (k10i11 : pathd (λ j0 → path A (a10i11 j0) (b10i11 j0)) k10011 k10111)
  (k1100i : pathd (λ j0 → path A (a1100i j0) (b1100i j0)) k11000 k11001)
  (k1101i : pathd (λ j0 → path A (a1101i j0) (b1101i j0)) k11010 k11011)
  (k110i0 : pathd (λ j0 → path A (a110i0 j0) (b110i0 j0)) k11000 k11010)
  (k110i1 : pathd (λ j0 → path A (a110i1 j0) (b110i1 j0)) k11001 k11011)
  (k1110i : pathd (λ j0 → path A (a1110i j0) (b1110i j0)) k11100 k11101)
  (k1111i : pathd (λ j0 → path A (a1111i j0) (b1111i j0)) k11110 k11111)
  (k111i0 : pathd (λ j0 → path A (a111i0 j0) (b111i0 j0)) k11100 k11110)
  (k111i1 : pathd (λ j0 → path A (a111i1 j0) (b111i1 j0)) k11101 k11111)
  (k11i00 : pathd (λ j0 → path A (a11i00 j0) (b11i00 j0)) k11000 k11100)
  (k11i01 : pathd (λ j0 → path A (a11i01 j0) (b11i01 j0)) k11001 k11101)
  (k11i10 : pathd (λ j0 → path A (a11i10 j0) (b11i10 j0)) k11010 k11110)
  (k11i11 : pathd (λ j0 → path A (a11i11 j0) (b11i11 j0)) k11011 k11111)
  (k1i000 : pathd (λ j0 → path A (a1i000 j0) (b1i000 j0)) k10000 k11000)
  (k1i001 : pathd (λ j0 → path A (a1i001 j0) (b1i001 j0)) k10001 k11001)
  (k1i010 : pathd (λ j0 → path A (a1i010 j0) (b1i010 j0)) k10010 k11010)
  (k1i011 : pathd (λ j0 → path A (a1i011 j0) (b1i011 j0)) k10011 k11011)
  (k1i100 : pathd (λ j0 → path A (a1i100 j0) (b1i100 j0)) k10100 k11100)
  (k1i101 : pathd (λ j0 → path A (a1i101 j0) (b1i101 j0)) k10101 k11101)
  (k1i110 : pathd (λ j0 → path A (a1i110 j0) (b1i110 j0)) k10110 k11110)
  (k1i111 : pathd (λ j0 → path A (a1i111 j0) (b1i111 j0)) k10111 k11111)
  (ki0000 : pathd (λ j0 → path A (ai0000 j0) (bi0000 j0)) k00000 k10000)
  (ki0001 : pathd (λ j0 → path A (ai0001 j0) (bi0001 j0)) k00001 k10001)
  (ki0010 : pathd (λ j0 → path A (ai0010 j0) (bi0010 j0)) k00010 k10010)
  (ki0011 : pathd (λ j0 → path A (ai0011 j0) (bi0011 j0)) k00011 k10011)
  (ki0100 : pathd (λ j0 → path A (ai0100 j0) (bi0100 j0)) k00100 k10100)
  (ki0101 : pathd (λ j0 → path A (ai0101 j0) (bi0101 j0)) k00101 k10101)
  (ki0110 : pathd (λ j0 → path A (ai0110 j0) (bi0110 j0)) k00110 k10110)
  (ki0111 : pathd (λ j0 → path A (ai0111 j0) (bi0111 j0)) k00111 k10111)
  (ki1000 : pathd (λ j0 → path A (ai1000 j0) (bi1000 j0)) k01000 k11000)
  (ki1001 : pathd (λ j0 → path A (ai1001 j0) (bi1001 j0)) k01001 k11001)
  (ki1010 : pathd (λ j0 → path A (ai1010 j0) (bi1010 j0)) k01010 k11010)
  (ki1011 : pathd (λ j0 → path A (ai1011 j0) (bi1011 j0)) k01011 k11011)
  (ki1100 : pathd (λ j0 → path A (ai1100 j0) (bi1100 j0)) k01100 k11100)
  (ki1101 : pathd (λ j0 → path A (ai1101 j0) (bi1101 j0)) k01101 k11101)
  (ki1110 : pathd (λ j0 → path A (ai1110 j0) (bi1110 j0)) k01110 k11110)
  (ki1111 : pathd (λ j0 → path A (ai1111 j0) (bi1111 j0)) k01111 k11111)
  (a00iii : pathd (λ j0 → pathd (λ j1 → path A (a000ii j0 j1) (a001ii j0 j1)) (a00i0i j0) (a00i1i j0)) a00ii0 a00ii1)
  (a01iii : pathd (λ j0 → pathd (λ j1 → path A (a010ii j0 j1) (a011ii j0 j1)) (a01i0i j0) (a01i1i j0)) a01ii0 a01ii1)
  (a0i0ii : pathd (λ j0 → pathd (λ j1 → path A (a000ii j0 j1) (a010ii j0 j1)) (a0i00i j0) (a0i01i j0)) a0i0i0 a0i0i1)
  (a0i1ii : pathd (λ j0 → pathd (λ j1 → path A (a001ii j0 j1) (a011ii j0 j1)) (a0i10i j0) (a0i11i j0)) a0i1i0 a0i1i1)
  (a0ii0i : pathd (λ j0 → pathd (λ j1 → path A (a00i0i j0 j1) (a01i0i j0 j1)) (a0i00i j0) (a0i10i j0)) a0ii00 a0ii01)
  (a0ii1i : pathd (λ j0 → pathd (λ j1 → path A (a00i1i j0 j1) (a01i1i j0 j1)) (a0i01i j0) (a0i11i j0)) a0ii10 a0ii11)
  (a0iii0 : pathd (λ j0 → pathd (λ j1 → path A (a00ii0 j0 j1) (a01ii0 j0 j1)) (a0i0i0 j0) (a0i1i0 j0)) a0ii00 a0ii10)
  (a0iii1 : pathd (λ j0 → pathd (λ j1 → path A (a00ii1 j0 j1) (a01ii1 j0 j1)) (a0i0i1 j0) (a0i1i1 j0)) a0ii01 a0ii11)
  (a10iii : pathd (λ j0 → pathd (λ j1 → path A (a100ii j0 j1) (a101ii j0 j1)) (a10i0i j0) (a10i1i j0)) a10ii0 a10ii1)
  (a11iii : pathd (λ j0 → pathd (λ j1 → path A (a110ii j0 j1) (a111ii j0 j1)) (a11i0i j0) (a11i1i j0)) a11ii0 a11ii1)
  (a1i0ii : pathd (λ j0 → pathd (λ j1 → path A (a100ii j0 j1) (a110ii j0 j1)) (a1i00i j0) (a1i01i j0)) a1i0i0 a1i0i1)
  (a1i1ii : pathd (λ j0 → pathd (λ j1 → path A (a101ii j0 j1) (a111ii j0 j1)) (a1i10i j0) (a1i11i j0)) a1i1i0 a1i1i1)
  (a1ii0i : pathd (λ j0 → pathd (λ j1 → path A (a10i0i j0 j1) (a11i0i j0 j1)) (a1i00i j0) (a1i10i j0)) a1ii00 a1ii01)
  (a1ii1i : pathd (λ j0 → pathd (λ j1 → path A (a10i1i j0 j1) (a11i1i j0 j1)) (a1i01i j0) (a1i11i j0)) a1ii10 a1ii11)
  (a1iii0 : pathd (λ j0 → pathd (λ j1 → path A (a10ii0 j0 j1) (a11ii0 j0 j1)) (a1i0i0 j0) (a1i1i0 j0)) a1ii00 a1ii10)
  (a1iii1 : pathd (λ j0 → pathd (λ j1 → path A (a10ii1 j0 j1) (a11ii1 j0 j1)) (a1i0i1 j0) (a1i1i1 j0)) a1ii01 a1ii11)
  (ai00ii : pathd (λ j0 → pathd (λ j1 → path A (a000ii j0 j1) (a100ii j0 j1)) (ai000i j0) (ai001i j0)) ai00i0 ai00i1)
  (ai01ii : pathd (λ j0 → pathd (λ j1 → path A (a001ii j0 j1) (a101ii j0 j1)) (ai010i j0) (ai011i j0)) ai01i0 ai01i1)
  (ai0i0i : pathd (λ j0 → pathd (λ j1 → path A (a00i0i j0 j1) (a10i0i j0 j1)) (ai000i j0) (ai010i j0)) ai0i00 ai0i01)
  (ai0i1i : pathd (λ j0 → pathd (λ j1 → path A (a00i1i j0 j1) (a10i1i j0 j1)) (ai001i j0) (ai011i j0)) ai0i10 ai0i11)
  (ai0ii0 : pathd (λ j0 → pathd (λ j1 → path A (a00ii0 j0 j1) (a10ii0 j0 j1)) (ai00i0 j0) (ai01i0 j0)) ai0i00 ai0i10)
  (ai0ii1 : pathd (λ j0 → pathd (λ j1 → path A (a00ii1 j0 j1) (a10ii1 j0 j1)) (ai00i1 j0) (ai01i1 j0)) ai0i01 ai0i11)
  (ai10ii : pathd (λ j0 → pathd (λ j1 → path A (a010ii j0 j1) (a110ii j0 j1)) (ai100i j0) (ai101i j0)) ai10i0 ai10i1)
  (ai11ii : pathd (λ j0 → pathd (λ j1 → path A (a011ii j0 j1) (a111ii j0 j1)) (ai110i j0) (ai111i j0)) ai11i0 ai11i1)
  (ai1i0i : pathd (λ j0 → pathd (λ j1 → path A (a01i0i j0 j1) (a11i0i j0 j1)) (ai100i j0) (ai110i j0)) ai1i00 ai1i01)
  (ai1i1i : pathd (λ j0 → pathd (λ j1 → path A (a01i1i j0 j1) (a11i1i j0 j1)) (ai101i j0) (ai111i j0)) ai1i10 ai1i11)
  (ai1ii0 : pathd (λ j0 → pathd (λ j1 → path A (a01ii0 j0 j1) (a11ii0 j0 j1)) (ai10i0 j0) (ai11i0 j0)) ai1i00 ai1i10)
  (ai1ii1 : pathd (λ j0 → pathd (λ j1 → path A (a01ii1 j0 j1) (a11ii1 j0 j1)) (ai10i1 j0) (ai11i1 j0)) ai1i01 ai1i11)
  (aii00i : pathd (λ j0 → pathd (λ j1 → path A (a0i00i j0 j1) (a1i00i j0 j1)) (ai000i j0) (ai100i j0)) aii000 aii001)
  (aii01i : pathd (λ j0 → pathd (λ j1 → path A (a0i01i j0 j1) (a1i01i j0 j1)) (ai001i j0) (ai101i j0)) aii010 aii011)
  (aii0i0 : pathd (λ j0 → pathd (λ j1 → path A (a0i0i0 j0 j1) (a1i0i0 j0 j1)) (ai00i0 j0) (ai10i0 j0)) aii000 aii010)
  (aii0i1 : pathd (λ j0 → pathd (λ j1 → path A (a0i0i1 j0 j1) (a1i0i1 j0 j1)) (ai00i1 j0) (ai10i1 j0)) aii001 aii011)
  (aii10i : pathd (λ j0 → pathd (λ j1 → path A (a0i10i j0 j1) (a1i10i j0 j1)) (ai010i j0) (ai110i j0)) aii100 aii101)
  (aii11i : pathd (λ j0 → pathd (λ j1 → path A (a0i11i j0 j1) (a1i11i j0 j1)) (ai011i j0) (ai111i j0)) aii110 aii111)
  (aii1i0 : pathd (λ j0 → pathd (λ j1 → path A (a0i1i0 j0 j1) (a1i1i0 j0 j1)) (ai01i0 j0) (ai11i0 j0)) aii100 aii110)
  (aii1i1 : pathd (λ j0 → pathd (λ j1 → path A (a0i1i1 j0 j1) (a1i1i1 j0 j1)) (ai01i1 j0) (ai11i1 j0)) aii101 aii111)
  (aiii00 : pathd (λ j0 → pathd (λ j1 → path A (a0ii00 j0 j1) (a1ii00 j0 j1)) (ai0i00 j0) (ai1i00 j0)) aii000 aii100)
  (aiii01 : pathd (λ j0 → pathd (λ j1 → path A (a0ii01 j0 j1) (a1ii01 j0 j1)) (ai0i01 j0) (ai1i01 j0)) aii001 aii101)
  (aiii10 : pathd (λ j0 → pathd (λ j1 → path A (a0ii10 j0 j1) (a1ii10 j0 j1)) (ai0i10 j0) (ai1i10 j0)) aii010 aii110)
  (aiii11 : pathd (λ j0 → pathd (λ j1 → path A (a0ii11 j0 j1) (a1ii11 j0 j1)) (ai0i11 j0) (ai1i11 j0)) aii011 aii111)
  (b00iii : pathd (λ j0 → pathd (λ j1 → path A (b000ii j0 j1) (b001ii j0 j1)) (b00i0i j0) (b00i1i j0)) b00ii0 b00ii1)
  (b01iii : pathd (λ j0 → pathd (λ j1 → path A (b010ii j0 j1) (b011ii j0 j1)) (b01i0i j0) (b01i1i j0)) b01ii0 b01ii1)
  (b0i0ii : pathd (λ j0 → pathd (λ j1 → path A (b000ii j0 j1) (b010ii j0 j1)) (b0i00i j0) (b0i01i j0)) b0i0i0 b0i0i1)
  (b0i1ii : pathd (λ j0 → pathd (λ j1 → path A (b001ii j0 j1) (b011ii j0 j1)) (b0i10i j0) (b0i11i j0)) b0i1i0 b0i1i1)
  (b0ii0i : pathd (λ j0 → pathd (λ j1 → path A (b00i0i j0 j1) (b01i0i j0 j1)) (b0i00i j0) (b0i10i j0)) b0ii00 b0ii01)
  (b0ii1i : pathd (λ j0 → pathd (λ j1 → path A (b00i1i j0 j1) (b01i1i j0 j1)) (b0i01i j0) (b0i11i j0)) b0ii10 b0ii11)
  (b0iii0 : pathd (λ j0 → pathd (λ j1 → path A (b00ii0 j0 j1) (b01ii0 j0 j1)) (b0i0i0 j0) (b0i1i0 j0)) b0ii00 b0ii10)
  (b0iii1 : pathd (λ j0 → pathd (λ j1 → path A (b00ii1 j0 j1) (b01ii1 j0 j1)) (b0i0i1 j0) (b0i1i1 j0)) b0ii01 b0ii11)
  (b10iii : pathd (λ j0 → pathd (λ j1 → path A (b100ii j0 j1) (b101ii j0 j1)) (b10i0i j0) (b10i1i j0)) b10ii0 b10ii1)
  (b11iii : pathd (λ j0 → pathd (λ j1 → path A (b110ii j0 j1) (b111ii j0 j1)) (b11i0i j0) (b11i1i j0)) b11ii0 b11ii1)
  (b1i0ii : pathd (λ j0 → pathd (λ j1 → path A (b100ii j0 j1) (b110ii j0 j1)) (b1i00i j0) (b1i01i j0)) b1i0i0 b1i0i1)
  (b1i1ii : pathd (λ j0 → pathd (λ j1 → path A (b101ii j0 j1) (b111ii j0 j1)) (b1i10i j0) (b1i11i j0)) b1i1i0 b1i1i1)
  (b1ii0i : pathd (λ j0 → pathd (λ j1 → path A (b10i0i j0 j1) (b11i0i j0 j1)) (b1i00i j0) (b1i10i j0)) b1ii00 b1ii01)
  (b1ii1i : pathd (λ j0 → pathd (λ j1 → path A (b10i1i j0 j1) (b11i1i j0 j1)) (b1i01i j0) (b1i11i j0)) b1ii10 b1ii11)
  (b1iii0 : pathd (λ j0 → pathd (λ j1 → path A (b10ii0 j0 j1) (b11ii0 j0 j1)) (b1i0i0 j0) (b1i1i0 j0)) b1ii00 b1ii10)
  (b1iii1 : pathd (λ j0 → pathd (λ j1 → path A (b10ii1 j0 j1) (b11ii1 j0 j1)) (b1i0i1 j0) (b1i1i1 j0)) b1ii01 b1ii11)
  (bi00ii : pathd (λ j0 → pathd (λ j1 → path A (b000ii j0 j1) (b100ii j0 j1)) (bi000i j0) (bi001i j0)) bi00i0 bi00i1)
  (bi01ii : pathd (λ j0 → pathd (λ j1 → path A (b001ii j0 j1) (b101ii j0 j1)) (bi010i j0) (bi011i j0)) bi01i0 bi01i1)
  (bi0i0i : pathd (λ j0 → pathd (λ j1 → path A (b00i0i j0 j1) (b10i0i j0 j1)) (bi000i j0) (bi010i j0)) bi0i00 bi0i01)
  (bi0i1i : pathd (λ j0 → pathd (λ j1 → path A (b00i1i j0 j1) (b10i1i j0 j1)) (bi001i j0) (bi011i j0)) bi0i10 bi0i11)
  (bi0ii0 : pathd (λ j0 → pathd (λ j1 → path A (b00ii0 j0 j1) (b10ii0 j0 j1)) (bi00i0 j0) (bi01i0 j0)) bi0i00 bi0i10)
  (bi0ii1 : pathd (λ j0 → pathd (λ j1 → path A (b00ii1 j0 j1) (b10ii1 j0 j1)) (bi00i1 j0) (bi01i1 j0)) bi0i01 bi0i11)
  (bi10ii : pathd (λ j0 → pathd (λ j1 → path A (b010ii j0 j1) (b110ii j0 j1)) (bi100i j0) (bi101i j0)) bi10i0 bi10i1)
  (bi11ii : pathd (λ j0 → pathd (λ j1 → path A (b011ii j0 j1) (b111ii j0 j1)) (bi110i j0) (bi111i j0)) bi11i0 bi11i1)
  (bi1i0i : pathd (λ j0 → pathd (λ j1 → path A (b01i0i j0 j1) (b11i0i j0 j1)) (bi100i j0) (bi110i j0)) bi1i00 bi1i01)
  (bi1i1i : pathd (λ j0 → pathd (λ j1 → path A (b01i1i j0 j1) (b11i1i j0 j1)) (bi101i j0) (bi111i j0)) bi1i10 bi1i11)
  (bi1ii0 : pathd (λ j0 → pathd (λ j1 → path A (b01ii0 j0 j1) (b11ii0 j0 j1)) (bi10i0 j0) (bi11i0 j0)) bi1i00 bi1i10)
  (bi1ii1 : pathd (λ j0 → pathd (λ j1 → path A (b01ii1 j0 j1) (b11ii1 j0 j1)) (bi10i1 j0) (bi11i1 j0)) bi1i01 bi1i11)
  (bii00i : pathd (λ j0 → pathd (λ j1 → path A (b0i00i j0 j1) (b1i00i j0 j1)) (bi000i j0) (bi100i j0)) bii000 bii001)
  (bii01i : pathd (λ j0 → pathd (λ j1 → path A (b0i01i j0 j1) (b1i01i j0 j1)) (bi001i j0) (bi101i j0)) bii010 bii011)
  (bii0i0 : pathd (λ j0 → pathd (λ j1 → path A (b0i0i0 j0 j1) (b1i0i0 j0 j1)) (bi00i0 j0) (bi10i0 j0)) bii000 bii010)
  (bii0i1 : pathd (λ j0 → pathd (λ j1 → path A (b0i0i1 j0 j1) (b1i0i1 j0 j1)) (bi00i1 j0) (bi10i1 j0)) bii001 bii011)
  (bii10i : pathd (λ j0 → pathd (λ j1 → path A (b0i10i j0 j1) (b1i10i j0 j1)) (bi010i j0) (bi110i j0)) bii100 bii101)
  (bii11i : pathd (λ j0 → pathd (λ j1 → path A (b0i11i j0 j1) (b1i11i j0 j1)) (bi011i j0) (bi111i j0)) bii110 bii111)
  (bii1i0 : pathd (λ j0 → pathd (λ j1 → path A (b0i1i0 j0 j1) (b1i1i0 j0 j1)) (bi01i0 j0) (bi11i0 j0)) bii100 bii110)
  (bii1i1 : pathd (λ j0 → pathd (λ j1 → path A (b0i1i1 j0 j1) (b1i1i1 j0 j1)) (bi01i1 j0) (bi11i1 j0)) bii101 bii111)
  (biii00 : pathd (λ j0 → pathd (λ j1 → path A (b0ii00 j0 j1) (b1ii00 j0 j1)) (bi0i00 j0) (bi1i00 j0)) bii000 bii100)
  (biii01 : pathd (λ j0 → pathd (λ j1 → path A (b0ii01 j0 j1) (b1ii01 j0 j1)) (bi0i01 j0) (bi1i01 j0)) bii001 bii101)
  (biii10 : pathd (λ j0 → pathd (λ j1 → path A (b0ii10 j0 j1) (b1ii10 j0 j1)) (bi0i10 j0) (bi1i10 j0)) bii010 bii110)
  (biii11 : pathd (λ j0 → pathd (λ j1 → path A (b0ii11 j0 j1) (b1ii11 j0 j1)) (bi0i11 j0) (bi1i11 j0)) bii011 bii111)
  (k000ii : pathd (λ j0 → pathd (λ j1 → path A (a000ii j0 j1) (b000ii j0 j1)) (k0000i j0) (k0001i j0)) k000i0 k000i1)
  (k001ii : pathd (λ j0 → pathd (λ j1 → path A (a001ii j0 j1) (b001ii j0 j1)) (k0010i j0) (k0011i j0)) k001i0 k001i1)
  (k00i0i : pathd (λ j0 → pathd (λ j1 → path A (a00i0i j0 j1) (b00i0i j0 j1)) (k0000i j0) (k0010i j0)) k00i00 k00i01)
  (k00i1i : pathd (λ j0 → pathd (λ j1 → path A (a00i1i j0 j1) (b00i1i j0 j1)) (k0001i j0) (k0011i j0)) k00i10 k00i11)
  (k00ii0 : pathd (λ j0 → pathd (λ j1 → path A (a00ii0 j0 j1) (b00ii0 j0 j1)) (k000i0 j0) (k001i0 j0)) k00i00 k00i10)
  (k00ii1 : pathd (λ j0 → pathd (λ j1 → path A (a00ii1 j0 j1) (b00ii1 j0 j1)) (k000i1 j0) (k001i1 j0)) k00i01 k00i11)
  (k010ii : pathd (λ j0 → pathd (λ j1 → path A (a010ii j0 j1) (b010ii j0 j1)) (k0100i j0) (k0101i j0)) k010i0 k010i1)
  (k011ii : pathd (λ j0 → pathd (λ j1 → path A (a011ii j0 j1) (b011ii j0 j1)) (k0110i j0) (k0111i j0)) k011i0 k011i1)
  (k01i0i : pathd (λ j0 → pathd (λ j1 → path A (a01i0i j0 j1) (b01i0i j0 j1)) (k0100i j0) (k0110i j0)) k01i00 k01i01)
  (k01i1i : pathd (λ j0 → pathd (λ j1 → path A (a01i1i j0 j1) (b01i1i j0 j1)) (k0101i j0) (k0111i j0)) k01i10 k01i11)
  (k01ii0 : pathd (λ j0 → pathd (λ j1 → path A (a01ii0 j0 j1) (b01ii0 j0 j1)) (k010i0 j0) (k011i0 j0)) k01i00 k01i10)
  (k01ii1 : pathd (λ j0 → pathd (λ j1 → path A (a01ii1 j0 j1) (b01ii1 j0 j1)) (k010i1 j0) (k011i1 j0)) k01i01 k01i11)
  (k0i00i : pathd (λ j0 → pathd (λ j1 → path A (a0i00i j0 j1) (b0i00i j0 j1)) (k0000i j0) (k0100i j0)) k0i000 k0i001)
  (k0i01i : pathd (λ j0 → pathd (λ j1 → path A (a0i01i j0 j1) (b0i01i j0 j1)) (k0001i j0) (k0101i j0)) k0i010 k0i011)
  (k0i0i0 : pathd (λ j0 → pathd (λ j1 → path A (a0i0i0 j0 j1) (b0i0i0 j0 j1)) (k000i0 j0) (k010i0 j0)) k0i000 k0i010)
  (k0i0i1 : pathd (λ j0 → pathd (λ j1 → path A (a0i0i1 j0 j1) (b0i0i1 j0 j1)) (k000i1 j0) (k010i1 j0)) k0i001 k0i011)
  (k0i10i : pathd (λ j0 → pathd (λ j1 → path A (a0i10i j0 j1) (b0i10i j0 j1)) (k0010i j0) (k0110i j0)) k0i100 k0i101)
  (k0i11i : pathd (λ j0 → pathd (λ j1 → path A (a0i11i j0 j1) (b0i11i j0 j1)) (k0011i j0) (k0111i j0)) k0i110 k0i111)
  (k0i1i0 : pathd (λ j0 → pathd (λ j1 → path A (a0i1i0 j0 j1) (b0i1i0 j0 j1)) (k001i0 j0) (k011i0 j0)) k0i100 k0i110)
  (k0i1i1 : pathd (λ j0 → pathd (λ j1 → path A (a0i1i1 j0 j1) (b0i1i1 j0 j1)) (k001i1 j0) (k011i1 j0)) k0i101 k0i111)
  (k0ii00 : pathd (λ j0 → pathd (λ j1 → path A (a0ii00 j0 j1) (b0ii00 j0 j1)) (k00i00 j0) (k01i00 j0)) k0i000 k0i100)
  (k0ii01 : pathd (λ j0 → pathd (λ j1 → path A (a0ii01 j0 j1) (b0ii01 j0 j1)) (k00i01 j0) (k01i01 j0)) k0i001 k0i101)
  (k0ii10 : pathd (λ j0 → pathd (λ j1 → path A (a0ii10 j0 j1) (b0ii10 j0 j1)) (k00i10 j0) (k01i10 j0)) k0i010 k0i110)
  (k0ii11 : pathd (λ j0 → pathd (λ j1 → path A (a0ii11 j0 j1) (b0ii11 j0 j1)) (k00i11 j0) (k01i11 j0)) k0i011 k0i111)
  (k100ii : pathd (λ j0 → pathd (λ j1 → path A (a100ii j0 j1) (b100ii j0 j1)) (k1000i j0) (k1001i j0)) k100i0 k100i1)
  (k101ii : pathd (λ j0 → pathd (λ j1 → path A (a101ii j0 j1) (b101ii j0 j1)) (k1010i j0) (k1011i j0)) k101i0 k101i1)
  (k10i0i : pathd (λ j0 → pathd (λ j1 → path A (a10i0i j0 j1) (b10i0i j0 j1)) (k1000i j0) (k1010i j0)) k10i00 k10i01)
  (k10i1i : pathd (λ j0 → pathd (λ j1 → path A (a10i1i j0 j1) (b10i1i j0 j1)) (k1001i j0) (k1011i j0)) k10i10 k10i11)
  (k10ii0 : pathd (λ j0 → pathd (λ j1 → path A (a10ii0 j0 j1) (b10ii0 j0 j1)) (k100i0 j0) (k101i0 j0)) k10i00 k10i10)
  (k10ii1 : pathd (λ j0 → pathd (λ j1 → path A (a10ii1 j0 j1) (b10ii1 j0 j1)) (k100i1 j0) (k101i1 j0)) k10i01 k10i11)
  (k110ii : pathd (λ j0 → pathd (λ j1 → path A (a110ii j0 j1) (b110ii j0 j1)) (k1100i j0) (k1101i j0)) k110i0 k110i1)
  (k111ii : pathd (λ j0 → pathd (λ j1 → path A (a111ii j0 j1) (b111ii j0 j1)) (k1110i j0) (k1111i j0)) k111i0 k111i1)
  (k11i0i : pathd (λ j0 → pathd (λ j1 → path A (a11i0i j0 j1) (b11i0i j0 j1)) (k1100i j0) (k1110i j0)) k11i00 k11i01)
  (k11i1i : pathd (λ j0 → pathd (λ j1 → path A (a11i1i j0 j1) (b11i1i j0 j1)) (k1101i j0) (k1111i j0)) k11i10 k11i11)
  (k11ii0 : pathd (λ j0 → pathd (λ j1 → path A (a11ii0 j0 j1) (b11ii0 j0 j1)) (k110i0 j0) (k111i0 j0)) k11i00 k11i10)
  (k11ii1 : pathd (λ j0 → pathd (λ j1 → path A (a11ii1 j0 j1) (b11ii1 j0 j1)) (k110i1 j0) (k111i1 j0)) k11i01 k11i11)
  (k1i00i : pathd (λ j0 → pathd (λ j1 → path A (a1i00i j0 j1) (b1i00i j0 j1)) (k1000i j0) (k1100i j0)) k1i000 k1i001)
  (k1i01i : pathd (λ j0 → pathd (λ j1 → path A (a1i01i j0 j1) (b1i01i j0 j1)) (k1001i j0) (k1101i j0)) k1i010 k1i011)
  (k1i0i0 : pathd (λ j0 → pathd (λ j1 → path A (a1i0i0 j0 j1) (b1i0i0 j0 j1)) (k100i0 j0) (k110i0 j0)) k1i000 k1i010)
  (k1i0i1 : pathd (λ j0 → pathd (λ j1 → path A (a1i0i1 j0 j1) (b1i0i1 j0 j1)) (k100i1 j0) (k110i1 j0)) k1i001 k1i011)
  (k1i10i : pathd (λ j0 → pathd (λ j1 → path A (a1i10i j0 j1) (b1i10i j0 j1)) (k1010i j0) (k1110i j0)) k1i100 k1i101)
  (k1i11i : pathd (λ j0 → pathd (λ j1 → path A (a1i11i j0 j1) (b1i11i j0 j1)) (k1011i j0) (k1111i j0)) k1i110 k1i111)
  (k1i1i0 : pathd (λ j0 → pathd (λ j1 → path A (a1i1i0 j0 j1) (b1i1i0 j0 j1)) (k101i0 j0) (k111i0 j0)) k1i100 k1i110)
  (k1i1i1 : pathd (λ j0 → pathd (λ j1 → path A (a1i1i1 j0 j1) (b1i1i1 j0 j1)) (k101i1 j0) (k111i1 j0)) k1i101 k1i111)
  (k1ii00 : pathd (λ j0 → pathd (λ j1 → path A (a1ii00 j0 j1) (b1ii00 j0 j1)) (k10i00 j0) (k11i00 j0)) k1i000 k1i100)
  (k1ii01 : pathd (λ j0 → pathd (λ j1 → path A (a1ii01 j0 j1) (b1ii01 j0 j1)) (k10i01 j0) (k11i01 j0)) k1i001 k1i101)
  (k1ii10 : pathd (λ j0 → pathd (λ j1 → path A (a1ii10 j0 j1) (b1ii10 j0 j1)) (k10i10 j0) (k11i10 j0)) k1i010 k1i110)
  (k1ii11 : pathd (λ j0 → pathd (λ j1 → path A (a1ii11 j0 j1) (b1ii11 j0 j1)) (k10i11 j0) (k11i11 j0)) k1i011 k1i111)
  (ki000i : pathd (λ j0 → pathd (λ j1 → path A (ai000i j0 j1) (bi000i j0 j1)) (k0000i j0) (k1000i j0)) ki0000 ki0001)
  (ki001i : pathd (λ j0 → pathd (λ j1 → path A (ai001i j0 j1) (bi001i j0 j1)) (k0001i j0) (k1001i j0)) ki0010 ki0011)
  (ki00i0 : pathd (λ j0 → pathd (λ j1 → path A (ai00i0 j0 j1) (bi00i0 j0 j1)) (k000i0 j0) (k100i0 j0)) ki0000 ki0010)
  (ki00i1 : pathd (λ j0 → pathd (λ j1 → path A (ai00i1 j0 j1) (bi00i1 j0 j1)) (k000i1 j0) (k100i1 j0)) ki0001 ki0011)
  (ki010i : pathd (λ j0 → pathd (λ j1 → path A (ai010i j0 j1) (bi010i j0 j1)) (k0010i j0) (k1010i j0)) ki0100 ki0101)
  (ki011i : pathd (λ j0 → pathd (λ j1 → path A (ai011i j0 j1) (bi011i j0 j1)) (k0011i j0) (k1011i j0)) ki0110 ki0111)
  (ki01i0 : pathd (λ j0 → pathd (λ j1 → path A (ai01i0 j0 j1) (bi01i0 j0 j1)) (k001i0 j0) (k101i0 j0)) ki0100 ki0110)
  (ki01i1 : pathd (λ j0 → pathd (λ j1 → path A (ai01i1 j0 j1) (bi01i1 j0 j1)) (k001i1 j0) (k101i1 j0)) ki0101 ki0111)
  (ki0i00 : pathd (λ j0 → pathd (λ j1 → path A (ai0i00 j0 j1) (bi0i00 j0 j1)) (k00i00 j0) (k10i00 j0)) ki0000 ki0100)
  (ki0i01 : pathd (λ j0 → pathd (λ j1 → path A (ai0i01 j0 j1) (bi0i01 j0 j1)) (k00i01 j0) (k10i01 j0)) ki0001 ki0101)
  (ki0i10 : pathd (λ j0 → pathd (λ j1 → path A (ai0i10 j0 j1) (bi0i10 j0 j1)) (k00i10 j0) (k10i10 j0)) ki0010 ki0110)
  (ki0i11 : pathd (λ j0 → pathd (λ j1 → path A (ai0i11 j0 j1) (bi0i11 j0 j1)) (k00i11 j0) (k10i11 j0)) ki0011 ki0111)
  (ki100i : pathd (λ j0 → pathd (λ j1 → path A (ai100i j0 j1) (bi100i j0 j1)) (k0100i j0) (k1100i j0)) ki1000 ki1001)
  (ki101i : pathd (λ j0 → pathd (λ j1 → path A (ai101i j0 j1) (bi101i j0 j1)) (k0101i j0) (k1101i j0)) ki1010 ki1011)
  (ki10i0 : pathd (λ j0 → pathd (λ j1 → path A (ai10i0 j0 j1) (bi10i0 j0 j1)) (k010i0 j0) (k110i0 j0)) ki1000 ki1010)
  (ki10i1 : pathd (λ j0 → pathd (λ j1 → path A (ai10i1 j0 j1) (bi10i1 j0 j1)) (k010i1 j0) (k110i1 j0)) ki1001 ki1011)
  (ki110i : pathd (λ j0 → pathd (λ j1 → path A (ai110i j0 j1) (bi110i j0 j1)) (k0110i j0) (k1110i j0)) ki1100 ki1101)
  (ki111i : pathd (λ j0 → pathd (λ j1 → path A (ai111i j0 j1) (bi111i j0 j1)) (k0111i j0) (k1111i j0)) ki1110 ki1111)
  (ki11i0 : pathd (λ j0 → pathd (λ j1 → path A (ai11i0 j0 j1) (bi11i0 j0 j1)) (k011i0 j0) (k111i0 j0)) ki1100 ki1110)
  (ki11i1 : pathd (λ j0 → pathd (λ j1 → path A (ai11i1 j0 j1) (bi11i1 j0 j1)) (k011i1 j0) (k111i1 j0)) ki1101 ki1111)
  (ki1i00 : pathd (λ j0 → pathd (λ j1 → path A (ai1i00 j0 j1) (bi1i00 j0 j1)) (k01i00 j0) (k11i00 j0)) ki1000 ki1100)
  (ki1i01 : pathd (λ j0 → pathd (λ j1 → path A (ai1i01 j0 j1) (bi1i01 j0 j1)) (k01i01 j0) (k11i01 j0)) ki1001 ki1101)
  (ki1i10 : pathd (λ j0 → pathd (λ j1 → path A (ai1i10 j0 j1) (bi1i10 j0 j1)) (k01i10 j0) (k11i10 j0)) ki1010 ki1110)
  (ki1i11 : pathd (λ j0 → pathd (λ j1 → path A (ai1i11 j0 j1) (bi1i11 j0 j1)) (k01i11 j0) (k11i11 j0)) ki1011 ki1111)
  (kii000 : pathd (λ j0 → pathd (λ j1 → path A (aii000 j0 j1) (bii000 j0 j1)) (k0i000 j0) (k1i000 j0)) ki0000 ki1000)
  (kii001 : pathd (λ j0 → pathd (λ j1 → path A (aii001 j0 j1) (bii001 j0 j1)) (k0i001 j0) (k1i001 j0)) ki0001 ki1001)
  (kii010 : pathd (λ j0 → pathd (λ j1 → path A (aii010 j0 j1) (bii010 j0 j1)) (k0i010 j0) (k1i010 j0)) ki0010 ki1010)
  (kii011 : pathd (λ j0 → pathd (λ j1 → path A (aii011 j0 j1) (bii011 j0 j1)) (k0i011 j0) (k1i011 j0)) ki0011 ki1011)
  (kii100 : pathd (λ j0 → pathd (λ j1 → path A (aii100 j0 j1) (bii100 j0 j1)) (k0i100 j0) (k1i100 j0)) ki0100 ki1100)
  (kii101 : pathd (λ j0 → pathd (λ j1 → path A (aii101 j0 j1) (bii101 j0 j1)) (k0i101 j0) (k1i101 j0)) ki0101 ki1101)
  (kii110 : pathd (λ j0 → pathd (λ j1 → path A (aii110 j0 j1) (bii110 j0 j1)) (k0i110 j0) (k1i110 j0)) ki0110 ki1110)
  (kii111 : pathd (λ j0 → pathd (λ j1 → path A (aii111 j0 j1) (bii111 j0 j1)) (k0i111 j0) (k1i111 j0)) ki0111 ki1111)
  (a0iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a00iii j0 j1 j2) (a01iii j0 j1 j2)) (a0i0ii j0 j1) (a0i1ii j0 j1)) (a0ii0i j0) (a0ii1i j0)) a0iii0 a0iii1)
  (a1iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a10iii j0 j1 j2) (a11iii j0 j1 j2)) (a1i0ii j0 j1) (a1i1ii j0 j1)) (a1ii0i j0) (a1ii1i j0)) a1iii0 a1iii1)
  (ai0iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a00iii j0 j1 j2) (a10iii j0 j1 j2)) (ai00ii j0 j1) (ai01ii j0 j1)) (ai0i0i j0) (ai0i1i j0)) ai0ii0 ai0ii1)
  (ai1iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a01iii j0 j1 j2) (a11iii j0 j1 j2)) (ai10ii j0 j1) (ai11ii j0 j1)) (ai1i0i j0) (ai1i1i j0)) ai1ii0 ai1ii1)
  (aii0ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0i0ii j0 j1 j2) (a1i0ii j0 j1 j2)) (ai00ii j0 j1) (ai10ii j0 j1)) (aii00i j0) (aii01i j0)) aii0i0 aii0i1)
  (aii1ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0i1ii j0 j1 j2) (a1i1ii j0 j1 j2)) (ai01ii j0 j1) (ai11ii j0 j1)) (aii10i j0) (aii11i j0)) aii1i0 aii1i1)
  (aiii0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0ii0i j0 j1 j2) (a1ii0i j0 j1 j2)) (ai0i0i j0 j1) (ai1i0i j0 j1)) (aii00i j0) (aii10i j0)) aiii00 aiii01)
  (aiii1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0ii1i j0 j1 j2) (a1ii1i j0 j1 j2)) (ai0i1i j0 j1) (ai1i1i j0 j1)) (aii01i j0) (aii11i j0)) aiii10 aiii11)
  (aiiii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0iii0 j0 j1 j2) (a1iii0 j0 j1 j2)) (ai0ii0 j0 j1) (ai1ii0 j0 j1)) (aii0i0 j0) (aii1i0 j0)) aiii00 aiii10)
  (aiiii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0iii1 j0 j1 j2) (a1iii1 j0 j1 j2)) (ai0ii1 j0 j1) (ai1ii1 j0 j1)) (aii0i1 j0) (aii1i1 j0)) aiii01 aiii11)
  (b0iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b00iii j0 j1 j2) (b01iii j0 j1 j2)) (b0i0ii j0 j1) (b0i1ii j0 j1)) (b0ii0i j0) (b0ii1i j0)) b0iii0 b0iii1)
  (b1iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b10iii j0 j1 j2) (b11iii j0 j1 j2)) (b1i0ii j0 j1) (b1i1ii j0 j1)) (b1ii0i j0) (b1ii1i j0)) b1iii0 b1iii1)
  (bi0iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b00iii j0 j1 j2) (b10iii j0 j1 j2)) (bi00ii j0 j1) (bi01ii j0 j1)) (bi0i0i j0) (bi0i1i j0)) bi0ii0 bi0ii1)
  (bi1iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b01iii j0 j1 j2) (b11iii j0 j1 j2)) (bi10ii j0 j1) (bi11ii j0 j1)) (bi1i0i j0) (bi1i1i j0)) bi1ii0 bi1ii1)
  (bii0ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0i0ii j0 j1 j2) (b1i0ii j0 j1 j2)) (bi00ii j0 j1) (bi10ii j0 j1)) (bii00i j0) (bii01i j0)) bii0i0 bii0i1)
  (bii1ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0i1ii j0 j1 j2) (b1i1ii j0 j1 j2)) (bi01ii j0 j1) (bi11ii j0 j1)) (bii10i j0) (bii11i j0)) bii1i0 bii1i1)
  (biii0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0ii0i j0 j1 j2) (b1ii0i j0 j1 j2)) (bi0i0i j0 j1) (bi1i0i j0 j1)) (bii00i j0) (bii10i j0)) biii00 biii01)
  (biii1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0ii1i j0 j1 j2) (b1ii1i j0 j1 j2)) (bi0i1i j0 j1) (bi1i1i j0 j1)) (bii01i j0) (bii11i j0)) biii10 biii11)
  (biiii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0iii0 j0 j1 j2) (b1iii0 j0 j1 j2)) (bi0ii0 j0 j1) (bi1ii0 j0 j1)) (bii0i0 j0) (bii1i0 j0)) biii00 biii10)
  (biiii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (b0iii1 j0 j1 j2) (b1iii1 j0 j1 j2)) (bi0ii1 j0 j1) (bi1ii1 j0 j1)) (bii0i1 j0) (bii1i1 j0)) biii01 biii11)
  (k00iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a00iii j0 j1 j2) (b00iii j0 j1 j2)) (k000ii j0 j1) (k001ii j0 j1)) (k00i0i j0) (k00i1i j0)) k00ii0 k00ii1)
  (k01iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a01iii j0 j1 j2) (b01iii j0 j1 j2)) (k010ii j0 j1) (k011ii j0 j1)) (k01i0i j0) (k01i1i j0)) k01ii0 k01ii1)
  (k0i0ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0i0ii j0 j1 j2) (b0i0ii j0 j1 j2)) (k000ii j0 j1) (k010ii j0 j1)) (k0i00i j0) (k0i01i j0)) k0i0i0 k0i0i1)
  (k0i1ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0i1ii j0 j1 j2) (b0i1ii j0 j1 j2)) (k001ii j0 j1) (k011ii j0 j1)) (k0i10i j0) (k0i11i j0)) k0i1i0 k0i1i1)
  (k0ii0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0ii0i j0 j1 j2) (b0ii0i j0 j1 j2)) (k00i0i j0 j1) (k01i0i j0 j1)) (k0i00i j0) (k0i10i j0)) k0ii00 k0ii01)
  (k0ii1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0ii1i j0 j1 j2) (b0ii1i j0 j1 j2)) (k00i1i j0 j1) (k01i1i j0 j1)) (k0i01i j0) (k0i11i j0)) k0ii10 k0ii11)
  (k0iii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0iii0 j0 j1 j2) (b0iii0 j0 j1 j2)) (k00ii0 j0 j1) (k01ii0 j0 j1)) (k0i0i0 j0) (k0i1i0 j0)) k0ii00 k0ii10)
  (k0iii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a0iii1 j0 j1 j2) (b0iii1 j0 j1 j2)) (k00ii1 j0 j1) (k01ii1 j0 j1)) (k0i0i1 j0) (k0i1i1 j0)) k0ii01 k0ii11)
  (k10iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a10iii j0 j1 j2) (b10iii j0 j1 j2)) (k100ii j0 j1) (k101ii j0 j1)) (k10i0i j0) (k10i1i j0)) k10ii0 k10ii1)
  (k11iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a11iii j0 j1 j2) (b11iii j0 j1 j2)) (k110ii j0 j1) (k111ii j0 j1)) (k11i0i j0) (k11i1i j0)) k11ii0 k11ii1)
  (k1i0ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1i0ii j0 j1 j2) (b1i0ii j0 j1 j2)) (k100ii j0 j1) (k110ii j0 j1)) (k1i00i j0) (k1i01i j0)) k1i0i0 k1i0i1)
  (k1i1ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1i1ii j0 j1 j2) (b1i1ii j0 j1 j2)) (k101ii j0 j1) (k111ii j0 j1)) (k1i10i j0) (k1i11i j0)) k1i1i0 k1i1i1)
  (k1ii0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1ii0i j0 j1 j2) (b1ii0i j0 j1 j2)) (k10i0i j0 j1) (k11i0i j0 j1)) (k1i00i j0) (k1i10i j0)) k1ii00 k1ii01)
  (k1ii1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1ii1i j0 j1 j2) (b1ii1i j0 j1 j2)) (k10i1i j0 j1) (k11i1i j0 j1)) (k1i01i j0) (k1i11i j0)) k1ii10 k1ii11)
  (k1iii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1iii0 j0 j1 j2) (b1iii0 j0 j1 j2)) (k10ii0 j0 j1) (k11ii0 j0 j1)) (k1i0i0 j0) (k1i1i0 j0)) k1ii00 k1ii10)
  (k1iii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (a1iii1 j0 j1 j2) (b1iii1 j0 j1 j2)) (k10ii1 j0 j1) (k11ii1 j0 j1)) (k1i0i1 j0) (k1i1i1 j0)) k1ii01 k1ii11)
  (ki00ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai00ii j0 j1 j2) (bi00ii j0 j1 j2)) (k000ii j0 j1) (k100ii j0 j1)) (ki000i j0) (ki001i j0)) ki00i0 ki00i1)
  (ki01ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai01ii j0 j1 j2) (bi01ii j0 j1 j2)) (k001ii j0 j1) (k101ii j0 j1)) (ki010i j0) (ki011i j0)) ki01i0 ki01i1)
  (ki0i0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai0i0i j0 j1 j2) (bi0i0i j0 j1 j2)) (k00i0i j0 j1) (k10i0i j0 j1)) (ki000i j0) (ki010i j0)) ki0i00 ki0i01)
  (ki0i1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai0i1i j0 j1 j2) (bi0i1i j0 j1 j2)) (k00i1i j0 j1) (k10i1i j0 j1)) (ki001i j0) (ki011i j0)) ki0i10 ki0i11)
  (ki0ii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai0ii0 j0 j1 j2) (bi0ii0 j0 j1 j2)) (k00ii0 j0 j1) (k10ii0 j0 j1)) (ki00i0 j0) (ki01i0 j0)) ki0i00 ki0i10)
  (ki0ii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai0ii1 j0 j1 j2) (bi0ii1 j0 j1 j2)) (k00ii1 j0 j1) (k10ii1 j0 j1)) (ki00i1 j0) (ki01i1 j0)) ki0i01 ki0i11)
  (ki10ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai10ii j0 j1 j2) (bi10ii j0 j1 j2)) (k010ii j0 j1) (k110ii j0 j1)) (ki100i j0) (ki101i j0)) ki10i0 ki10i1)
  (ki11ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai11ii j0 j1 j2) (bi11ii j0 j1 j2)) (k011ii j0 j1) (k111ii j0 j1)) (ki110i j0) (ki111i j0)) ki11i0 ki11i1)
  (ki1i0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai1i0i j0 j1 j2) (bi1i0i j0 j1 j2)) (k01i0i j0 j1) (k11i0i j0 j1)) (ki100i j0) (ki110i j0)) ki1i00 ki1i01)
  (ki1i1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai1i1i j0 j1 j2) (bi1i1i j0 j1 j2)) (k01i1i j0 j1) (k11i1i j0 j1)) (ki101i j0) (ki111i j0)) ki1i10 ki1i11)
  (ki1ii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai1ii0 j0 j1 j2) (bi1ii0 j0 j1 j2)) (k01ii0 j0 j1) (k11ii0 j0 j1)) (ki10i0 j0) (ki11i0 j0)) ki1i00 ki1i10)
  (ki1ii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (ai1ii1 j0 j1 j2) (bi1ii1 j0 j1 j2)) (k01ii1 j0 j1) (k11ii1 j0 j1)) (ki10i1 j0) (ki11i1 j0)) ki1i01 ki1i11)
  (kii00i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii00i j0 j1 j2) (bii00i j0 j1 j2)) (k0i00i j0 j1) (k1i00i j0 j1)) (ki000i j0) (ki100i j0)) kii000 kii001)
  (kii01i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii01i j0 j1 j2) (bii01i j0 j1 j2)) (k0i01i j0 j1) (k1i01i j0 j1)) (ki001i j0) (ki101i j0)) kii010 kii011)
  (kii0i0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii0i0 j0 j1 j2) (bii0i0 j0 j1 j2)) (k0i0i0 j0 j1) (k1i0i0 j0 j1)) (ki00i0 j0) (ki10i0 j0)) kii000 kii010)
  (kii0i1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii0i1 j0 j1 j2) (bii0i1 j0 j1 j2)) (k0i0i1 j0 j1) (k1i0i1 j0 j1)) (ki00i1 j0) (ki10i1 j0)) kii001 kii011)
  (kii10i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii10i j0 j1 j2) (bii10i j0 j1 j2)) (k0i10i j0 j1) (k1i10i j0 j1)) (ki010i j0) (ki110i j0)) kii100 kii101)
  (kii11i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii11i j0 j1 j2) (bii11i j0 j1 j2)) (k0i11i j0 j1) (k1i11i j0 j1)) (ki011i j0) (ki111i j0)) kii110 kii111)
  (kii1i0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii1i0 j0 j1 j2) (bii1i0 j0 j1 j2)) (k0i1i0 j0 j1) (k1i1i0 j0 j1)) (ki01i0 j0) (ki11i0 j0)) kii100 kii110)
  (kii1i1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aii1i1 j0 j1 j2) (bii1i1 j0 j1 j2)) (k0i1i1 j0 j1) (k1i1i1 j0 j1)) (ki01i1 j0) (ki11i1 j0)) kii101 kii111)
  (kiii00 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aiii00 j0 j1 j2) (biii00 j0 j1 j2)) (k0ii00 j0 j1) (k1ii00 j0 j1)) (ki0i00 j0) (ki1i00 j0)) kii000 kii100)
  (kiii01 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aiii01 j0 j1 j2) (biii01 j0 j1 j2)) (k0ii01 j0 j1) (k1ii01 j0 j1)) (ki0i01 j0) (ki1i01 j0)) kii001 kii101)
  (kiii10 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aiii10 j0 j1 j2) (biii10 j0 j1 j2)) (k0ii10 j0 j1) (k1ii10 j0 j1)) (ki0i10 j0) (ki1i10 j0)) kii010 kii110)
  (kiii11 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → path A (aiii11 j0 j1 j2) (biii11 j0 j1 j2)) (k0ii11 j0 j1) (k1ii11 j0 j1)) (ki0i11 j0) (ki1i11 j0)) kii011 kii111)
  (aiiiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (a0iiii j0 j1 j2 j3) (a1iiii j0 j1 j2 j3)) (ai0iii j0 j1 j2) (ai1iii j0 j1 j2)) (aii0ii j0 j1) (aii1ii j0 j1)) (aiii0i j0) (aiii1i j0)) aiiii0 aiiii1)
  (k0iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (a0iiii j0 j1 j2 j3) (b0iiii j0 j1 j2 j3)) (k00iii j0 j1 j2) (k01iii j0 j1 j2)) (k0i0ii j0 j1) (k0i1ii j0 j1)) (k0ii0i j0) (k0ii1i j0)) k0iii0 k0iii1)
  (k1iiii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (a1iiii j0 j1 j2 j3) (b1iiii j0 j1 j2 j3)) (k10iii j0 j1 j2) (k11iii j0 j1 j2)) (k1i0ii j0 j1) (k1i1ii j0 j1)) (k1ii0i j0) (k1ii1i j0)) k1iii0 k1iii1)
  (ki0iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (ai0iii j0 j1 j2 j3) (bi0iii j0 j1 j2 j3)) (k00iii j0 j1 j2) (k10iii j0 j1 j2)) (ki00ii j0 j1) (ki01ii j0 j1)) (ki0i0i j0) (ki0i1i j0)) ki0ii0 ki0ii1)
  (ki1iii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (ai1iii j0 j1 j2 j3) (bi1iii j0 j1 j2 j3)) (k01iii j0 j1 j2) (k11iii j0 j1 j2)) (ki10ii j0 j1) (ki11ii j0 j1)) (ki1i0i j0) (ki1i1i j0)) ki1ii0 ki1ii1)
  (kii0ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aii0ii j0 j1 j2 j3) (bii0ii j0 j1 j2 j3)) (k0i0ii j0 j1 j2) (k1i0ii j0 j1 j2)) (ki00ii j0 j1) (ki10ii j0 j1)) (kii00i j0) (kii01i j0)) kii0i0 kii0i1)
  (kii1ii : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aii1ii j0 j1 j2 j3) (bii1ii j0 j1 j2 j3)) (k0i1ii j0 j1 j2) (k1i1ii j0 j1 j2)) (ki01ii j0 j1) (ki11ii j0 j1)) (kii10i j0) (kii11i j0)) kii1i0 kii1i1)
  (kiii0i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aiii0i j0 j1 j2 j3) (biii0i j0 j1 j2 j3)) (k0ii0i j0 j1 j2) (k1ii0i j0 j1 j2)) (ki0i0i j0 j1) (ki1i0i j0 j1)) (kii00i j0) (kii10i j0)) kiii00 kiii01)
  (kiii1i : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aiii1i j0 j1 j2 j3) (biii1i j0 j1 j2 j3)) (k0ii1i j0 j1 j2) (k1ii1i j0 j1 j2)) (ki0i1i j0 j1) (ki1i1i j0 j1)) (kii01i j0) (kii11i j0)) kiii10 kiii11)
  (kiiii0 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aiiii0 j0 j1 j2 j3) (biiii0 j0 j1 j2 j3)) (k0iii0 j0 j1 j2) (k1iii0 j0 j1 j2)) (ki0ii0 j0 j1) (ki1ii0 j0 j1)) (kii0i0 j0) (kii1i0 j0)) kiii00 kiii10)
  (kiiii1 : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (aiiii1 j0 j1 j2 j3) (biiii1 j0 j1 j2 j3)) (k0iii1 j0 j1 j2) (k1iii1 j0 j1 j2)) (ki0ii1 j0 j1) (ki1ii1 j0 j1)) (kii0i1 j0) (kii1i1 j0)) kiii01 kiii11)
  : pathd (λ j0 → pathd (λ j1 → pathd (λ j2 → pathd (λ j3 → path A (b0iiii j0 j1 j2 j3) (b1iiii j0 j1 j2 j3)) (bi0iii j0 j1 j2) (bi1iii j0 j1 j2)) (bii0ii j0 j1) (bii1ii j0 j1)) (biii0i j0) (biii1i j0)) biiii0 biiii1
  =
  λ j0 j1 j2 j3 j4 → comp 0 1 (aiiiii j0 j1 j2 j3 j4) [
  | j0 = 0 → kiiii0 j1 j2 j3 j4
  | j0 = 1 → kiiii1 j1 j2 j3 j4
  | j1 = 0 → kiii0i j0 j2 j3 j4
  | j1 = 1 → kiii1i j0 j2 j3 j4
  | j2 = 0 → kii0ii j0 j1 j3 j4
  | j2 = 1 → kii1ii j0 j1 j3 j4
  | j3 = 0 → ki0iii j0 j1 j2 j4
  | j3 = 1 → ki1iii j0 j1 j2 j4
  | j4 = 0 → k0iiii j0 j1 j2 j3
  | j4 = 1 → k1iiii j0 j1 j2 j3
  ]