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