(A B : Type) : (A = B) <~> (A <~> B) := (equiv_path_universe A B)^-1%equiv.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.