{A B} {f g : A -> B} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} {s : PathSquare px0 px1 p0x p1x} {b00 : f a00 = g a00} {b01 : f a01 = g a01} {b10 : f a10 = g a10} {b11 : f a11 = g a11} {qx0 : DPath (fun x => f x = g x) px0 b00 b10} {qx1 : DPath (fun x => f x = g x) px1 b01 b11} {q0x : DPath (fun x => f x = g x) p0x b00 b01} {q1x : DPath (fun x => f x = g x) p1x b10 b11} : DPathSquare (fun x => f x = g x) s qx0 qx1 q0x q1x <~> PathCube (sq_dp qx0) (sq_dp qx1) (sq_dp q0x) (sq_dp q1x) (sq_ap f s) (sq_ap g s). Proof. destruct s. apply cu_GG1. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.