(qx0 : DPath P px0 b00 b10) (q0x : DPath P p0x b00 b01) (q1x : DPath P p1x b10 b11) : {qx1 : DPath P px1 b01 b11 & DPathSquare P s qx0 qx1 q0x q1x}. Proof. destruct s; apply sq_fill_r. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.