{A} (P : A -> Type) {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} (s : px0 @ p1x = p0x @ px1) {b00 b10 b01 b11} {qx0 : DPath P px0 b00 b10} {qx1 : DPath P px1 b01 b11} {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11} : DPath (fun p => DPath P p b00 b11) s (qx0 @Dp q1x) (q0x @Dp qx1) <~> DPathSquare P (sq_path s) qx0 qx1 q0x q1x. Proof. set (s' := sq_path s). rewrite <- (eissect sq_path s : sq_path^-1 s' = s). clearbody s'; clear s. destruct s'; cbn. apply sq_path. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.