fact: Definition pi_prod' {n : nat} (X Y : pType) : pPi n (X * Y) <~>* (pPi n X) * (pPi n Y).
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat