equiv_dc_const' {A B : Type} {x000 x010 x100 x110 x001 x011 x101 x111 : A} {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100} {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111} {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001} {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111} {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i} {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11} {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11} {cube : PathCube s0ii s1ii sii0 sii1 si0i si1i} {b000 b010 b100 b110 b001 b011 b101 b111 : B} {bp0i0 : DPath (fun _ => B) p0i0 b000 b010} {bp1i0 : DPath (fun _ => B) p1i0 b100 b110} {bpi00 : DPath (fun _ => B) pi00 b000 b100} {bpi10 : DPath (fun _ => B) pi10 b010 b110} {bp0i1 : DPath (fun _ => B) p0i1 b001 b011} {bp1i1 : DPath (fun _ => B) p1i1 b101 b111} {bpi01 : DPath (fun _ => B) pi01 b001 b101} {bpi11 : DPath (fun _ => B) pi11 b011 b111} {bp00i : DPath (fun _ => B) p00i b000 b001} {bp01i : DPath (fun _ => B) p01i b010 b011} {bp10i : DPath (fun _ => B) p10i b100 b101} {bp11i : DPath (fun _ => B) p11i b110 b111} {bs0ii : DPathSquare (fun _ => B) s0ii bp0i0 bp0i1 bp00i bp01i} {bs1ii : DPathSquare (fun _ => B) s1ii bp1i0 bp1i1 bp10i bp11i} {bsii0 : DPathSquare (fun _ => B) sii0 bp0i0 bp1i0 bpi00 bpi10} {bsii1 : DPathSquare (fun _ => B) sii1 bp0i1 bp1i1 bpi01 bpi11} {bsi0i : DPathSquare (fun _ => B) si0i bp00i bp10i bpi00 bpi01} {bsi1i : DPathSquare (fun _ => B) si1i bp01i bp11i bpi10 bpi11} : PathCube (ds_const'^-1 bs0ii) (ds_const'^-1 bs1ii) (ds_const'^-1 bsii0) (ds_const'^-1 bsii1) (ds_const'^-1 bsi0i) (ds_const'^-1 bsi1i) <~> DPathCube (fun _ => B) cube bs0ii bs1ii bsii0 bsii1 bsi0i bsi1i. Proof. by destruct cube. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Cubical.PathCube.