`{ua : Univalence} {X : Type} (R' R : RetractOf X) : PathRetractOf X R' R <~> R' = R. Proof. revert R' R; apply (equiv_path_issig_contr (issig_retractof X)). { intros [A [r [s H]]]; cbn. exists equiv_idmap. exists (fun x => 1%path). exists (fun x => 1%path). cbn. exact (fun a => equiv_p1_1q (ap_idmap (H a))). } intros [A [r [s H]]]; cbn. unfold PathRetractOf. contr_sigsig A (equiv_idmap A); cbn. contr_sigsig r (fun x:X => idpath (r x)); cbn. contr_sigsig s (fun x:A => idpath (s x)); cbn. refine (contr_equiv' {K : r o s == idmap & H == K} _). apply equiv_functor_sigma_id; intros K. apply equiv_functor_forall_id; intros a; cbn. apply equiv_concat_lr. - refine (concat_p1 _ @ ap_idmap (H a)). - symmetry; apply concat_1p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.