`{Univalence} (fact fact' : Factorization) : PathFactorization fact fact' <~> fact = fact'. Proof. refine (_ oE (issig_PathFactorization fact fact')^-1). revert fact fact'; apply (equiv_path_issig_contr issig_Factorization). { intros [I [f1 [f2 [ff [oc1 oc2]]]]]. exists (equiv_idmap I); cbn. exists (fun x:A => 1%path); cbn. exists (fun x:I => 1%path); cbn. intros; apply concat_1p. } intros [I [f1 [f2 [ff [oc1 oc2]]]]]. contr_sigsig I (equiv_idmap I); cbn. contr_sigsig f1 (fun x:A => idpath (f1 x)); cbn. contr_sigsig f2 (fun x:I => idpath (f2 x)); cbn. refine (contr_equiv' {ff' : f2 o f1 == f & ff == ff'} _). symmetry; srefine (equiv_functor_sigma' (equiv_sigma_contr _) _). { intros h; cbn. srefine (@istrunc_sigma _ _ _ _ _); [ | intros a]; apply contr_inhabited_hprop; try exact _; assumption. } intros [ff' [oc1' oc2']]; cbn. refine (equiv_functor_forall' (equiv_idmap _) _); intros a. refine (equiv_path_inverse _ _ oE _). apply equiv_concat_l; symmetry; apply concat_1p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.