fact: Definition joinrecdata_0gpd_fun (A B : Type) : Fun11 Type ZeroGpd := Build_Fun11 _ _ (joinrecdata_0gpd A B).
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core