fact: Definition contr_retract {X Y : Type} `{Contr X} (r : X -> Y) (s : Y -> X) (h : forall y, r (s y) = y) : Contr Y := Build_Contr _ (r (center X)) (fun y => (ap r (contr _)) @ h _).
imports: Overture PathGroupoids