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