(P : Type) (pb : P) (pla plb : pb = pb) (ps : PathSquare pla pla plb plb) : Torus -> P := Torus_ind _ pb (dp_const pla) (dp_const plb) (ds_const ps).
Require Import Basics.Overture Basics.Equivalences Cubical.DPath