fact: Definition Join (A : Type@{i}) (B : Type@{j}) := Pushout@{k i j k} (@fst A B) (@snd A B).
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core