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