{X Y : Type} (R : RetractOf X) (f : X -> Y) (g : retract_type R -> Y) (p : g o retract_retr R == f) (y : Y) : RetractOf (hfiber f y). Proof. destruct R as [A r s H]; simpl in *. simple refine (Build_RetractOf (hfiber f y) (hfiber g y) _ _ _). - intros [x q]. exists (r x). exact (p x @ q). - intros [a q]. exists (s a). exact ((p (s a))^ @ ap g (H a) @ q). - intros [a q]. simple refine (path_sigma' _ _ _). + exact (H a). + abstract ( rewrite transport_paths_Fl, !concat_p_pp, concat_pp_V, concat_Vp, concat_1p; reflexivity). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.