(X : Type) (R' R : RetractOf X) := { Ap : retract_type R' <~> retract_type R & { rp : Ap o retract_retr R' == retract_retr R & { sp : retract_sect R' o Ap^-1 == retract_sect R & forall a, ap Ap (retract_issect R' (Ap^-1 a)) @ eisretr Ap a = rp (retract_sect R' (Ap^-1 a)) @ ap (retract_retr R) (sp a) @ retract_issect R a } } }.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.