{A B : Type} {a00 a10 a01 a11 : A} (f f' : A -> B) (h : f == f') {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} (s : PathSquare px0 px1 p0x p1x) : PathCube (sq_ap f s) (sq_ap f' s) (ap_nat h _) apn apn apn. Proof. destruct s as [x]; cbn; by destruct (h x). Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.