fact: Definition joinrecdata_sym (A B P : Type) : joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core