A {B C} (f : B <~> C) : equiv_path (A * B) (A * C) (ap (prod A) (path_universe f)) = equiv_functor_prod_l f. Proof. revert f. equiv_intro (equiv_path B C) f. rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f). destruct f. apply path_equiv, path_arrow; intros x; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.