{A B : Type} (f : A <~> B) : equiv_path2_universe f f (fun x => 1) = 1. Proof. simpl. rewrite concat_1p, concat_p1, path_forall_1, path_sigma_hprop_1. reflexivity. Qed.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.