{X : Type} (R : RetractOf X) {B : Type} (f : retract_type R -> B) `{feq : IsEquiv _ _ f} : RetractOf X. Proof. destruct R as [A r s H]; refine (Build_RetractOf X B (f o r) (s o f^-1) _); intros x. exact (ap f (H (f^-1 x)) @ eisretr f x). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.