(p0x : a00 = a01) (p1x : a10 = a11) : (a00 = a10) <~> (a01 = a11). Proof. srapply equiv_adjointify. - intros px0; exact (sq_fill_r px0 p0x p1x).1. - intros px1; exact (sq_fill_l px1 p0x p1x).1. - intros px1. exact (sq_fill_r_uniq (sq_fill_r _ p0x p1x).2 (sq_fill_l px1 p0x p1x).2). - intros px0. exact (sq_fill_l_uniq (sq_fill_l _ p0x p1x).2 (sq_fill_r px0 p0x p1x).2). Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.