{A B C D : Type} (f : A -> B -> C) (g : C -> D) {a a' : A} (p : a = a') {b b' : B} (q : b = b') : PathCube (sq_ap011 (fun x y => g (f x y)) p q) (sq_ap g (sq_ap011 f p q)) apcs apcs apcs apcs. Proof. by destruct p, q. Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.