fact: Definition equiv_retractof {X : Type} (R : RetractOf X) {B : Type} (f : retract_type R -> B) `{feq : IsEquiv _ _ f} : RetractOf X.
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny