fact: Definition joinrecdata_sym_inv (A B P : Type) : joinrecdata_sym B A P $o joinrecdata_sym A B P $== Id _.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core