{A B : Type} (f : A -> B) {c1f : class1 factsys f} (P : B -> Type) (c2P : class2 factsys (@pr1 B P)) (d : forall a:A, P (f a)) : ExtensionAlong f P d. Proof. pose (e := lift_factsys factsys f c1f pr1 c2P (fun a => (f a ; d a)) idmap (fun a => 1)). pose (e2 := lift_factsys_tri2 factsys f c1f pr1 c2P (fun a => (f a ; d a)) idmap (fun a => 1)). exists (fun a => (e2 a) # (e a).2). intros a. pose (e1 := lift_factsys_tri1 factsys f c1f pr1 c2P (fun a => (f a ; d a)) idmap (fun a => 1) a : e (f a) = (f a ; d a)). pose (e3 := moveL_M1 _ _ (((ap_V _ _)^ @@ 1) @ lift_factsys_square factsys f c1f pr1 c2P (fun a => (f a ; d a)) idmap (fun a => 1) a) : e2 (f a) = pr1_path e1). refine (ap (fun p => transport P p (e (f a)).2) e3 @ _). exact (pr2_path e1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.