`{Funext} {X Y Z} (f : X -> Y) (g : Y -> Z) : class1 factsys f -> class1 factsys (g o f) -> class1 factsys g. Proof. intros c1f c1gf. destruct (factor factsys g) as [I g1 g2 gf c1g1 c2g2]. pose (fact := Build_Factorization' (g o f) Z (g o f) (idmap) (fun x => 1) c1gf (class2_isequiv factsys idmap)). pose (fact' := Build_Factorization' (g o f) I (g1 o f) g2 (fun x => gf (f x)) (class1_compose factsys f g1 c1f c1g1) c2g2). destruct (path_factor factsys (g o f) fact' fact) as [q q1 q2 qf]; simpl in *. refine (transport (class1 factsys) (path_arrow _ _ gf) _). refine (class1_compose factsys g1 g2 c1g1 _). apply class1_isequiv. apply (isequiv_homotopic _ (fun i => (q2 i)^)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.