{A} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} {s s' : PathSquare px0 px1 p0x p1x} : s = s' <~> PathCube s s' hr hr hr hr. Proof. destruct s. refine (cu_path oE _). refine (equiv_concat_l (sq_concat_h_1s (sq_concat_h 1%square (tr s')) (p0y:=1) (p1y:=1)) _ oE _). refine (equiv_concat_l (sq_concat_h_1s (tr s') (p0y:=1) (p1y:=1)) _ oE _). refine (equiv_moveR_equiv_M (f:=tr) _ _ oE _). apply equiv_path_inverse. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.