fact: Definition equiv_join_empty_left A : Join Empty A <~> A := equiv_join_empty_right _ oE equiv_join_sym _ _.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core