fact: Definition jc_factors@{} : jc_factor2 o jc_factor1 == f.
imports: HoTT.Basics HoTT.Types HoTT.Cubical.DPath HFiber Extensions Factorization Limits.Pullback Modality Accessible Descent Truncations.Core Homotopy.Suspension