retractof_equiv' {X Y : Type} (f : X <~> Y) : RetractOf X -> RetractOf Y := retractof_equiv f.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.