fact: Definition joinr {A B} : B -> Join A B := fun b => @pushr (A*B) A B fst snd b.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core