`{ua : Univalence} {X : Type} {R' R : RetractOf X} Ap rp sp Hp : R' = R := equiv_path_retractof R' R (Ap;rp;sp;Hp).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.