(X : Type) : { A : Type & {r : X -> A & {s : A -> X & r o s == idmap }}} <~> RetractOf X. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.