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