fact: Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D) : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core