{A} {B : A -> Type} (f : forall a, B a) {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x p1x} (s : PathSquare px0 px1 p0x p1x) : DPathSquare B s (apD f px0) (apD f px1) (apD f p0x) (apD f p1x). Proof. by destruct s. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.