`{Funext} {X Y Z} (f : X -> Y) (g : Y -> Z) : class2 factsys g -> class2 factsys (g o f) -> class2 factsys f. Proof. intros c2g c2gf. destruct (factor factsys f) as [I f1 f2 ff c1f1 c2f2]. pose (fact := Build_Factorization' (g o f) X (idmap) (g o f) (fun x => 1) (class1_isequiv factsys idmap) c2gf). pose (fact' := Build_Factorization' (g o f) I f1 (g o f2) (fun x => ap g (ff x)) c1f1 (class2_compose factsys f2 g c2f2 c2g)). destruct (path_factor factsys (g o f) fact fact') as [q q1 q2 qf]; simpl in *. refine (transport (class2 factsys) (path_arrow _ _ ff) _). refine (class2_compose factsys f1 f2 _ c2f2). apply class2_isequiv. apply (isequiv_homotopic _ q1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.