{A B : Type} {f g : A <~> B} {p q : f == g} : (p == q) -> (path2_universe p = path2_universe q) := equiv_path3_universe p q.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.