{A B : Type} {x1 x2 : A} {a00 a01 a10 a11 : A -> B} {px0 : a00 == a10} {px1 : a01 == a11} {p0x : a00 == a01} {p1x : a10 == a11} {f1 : PathSquare (px0 x1) (px1 x1) (p0x x1) (p1x x1)} {f2 : PathSquare (px0 x2) (px1 x2) (p0x x2) (p1x x2)} {p : x1 = x2} : PathCube f1 f2 (sq_dp (apD px0 p)) (sq_dp (apD px1 p)) (sq_dp (apD p0x p)) (sq_dp (apD p1x p)) <~> DPath (fun x => PathSquare (px0 x) (px1 x) (p0x x) (p1x x)) p f1 f2. Proof. destruct p; symmetry; exact cu_G11. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.