{A} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} : px0 @ p1x = p0x @ px1 <~> PathSquare px0 px1 p0x p1x. Proof. snrapply Build_Equiv. { destruct p0x, p1x. intro e. generalize (e @ concat_1p _). intro e'. destruct e', px0. exact sq_id. } srapply isequiv_adjointify; try by intros []. destruct p0x, p1x. intros e. pattern e. pose (e' := e @ concat_1p _). pose (e'' := e' @ (concat_1p _)^). refine (@transport _ _ e'' e _ _). - subst e' e''; hott_simpl. - clearbody e'; clear e. destruct e', px0. reflexivity. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.