p o lift_factsys == g. Proof. intros x. refine (q2 _ @ _). transitivity (g2 (g1 x)). + apply ap, eisretr. + apply gf. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.