{X : Type} (R : RetractOf X) : (X -> X) := retract_sect R o retract_retr R.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.