lift_factsys o i == f. Proof. intros x. refine (ap (f2 o q^-1) (q1 x)^ @ _). transitivity (f2 (f1 x)). + apply ap, eissect. + apply ff. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.