{X : Type} (R : RetractOf X ) (contra : Contr X) : Contr (retract_type R ) := contr_retract (retract_retr R) (retract_sect R) (retract_issect R).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.