fact: Definition join_power (A : Type@{u}) (n : nat) : Type@{u} := nat_iter n (Join A) (Empty : Type@{u}).
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core