{q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11} : (DPath P px0 b00 b10) <~> (DPath P px1 b01 b11). Proof. srapply equiv_adjointify. - intros qx0; exact (ds_fill_r qx0 q0x q1x).1. - intros qx1; exact (ds_fill_l qx1 q0x q1x).1. - intros qx1. exact (ds_fill_r_uniq (ds_fill_r _ q0x q1x).2 (ds_fill_l qx1 q0x q1x).2). - intros qx0. exact (ds_fill_l_uniq (ds_fill_l _ q0x q1x).2 (ds_fill_r qx0 q0x q1x).2). Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.