{A B C : Type} {f1 f2 : B <~> C} (p : f1 == f2) (g : A <~> B) : equiv_path2_universe (f1 o g) (f2 o g) (fun a => (p (g a))) = path_universe_compose g f1 @ whiskerL (path_universe g) (path2_universe p) @ (path_universe_compose g f2)^.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.