fact: Definition joinrecdata_sym_natequiv (A B : Type) : NatEquiv (joinrecdata_0gpd_fun A B) (joinrecdata_0gpd_fun B A).
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core