`{Funext} (A : Type) : IsHProp A <~> (forall (x y : A), x = y). Proof. rapply (equiv_iff_hprop (@path_ishprop A) (@hprop_allpath A)). apply hprop_allpath; intros f g. funext x y. pose (C := Build_Contr A x (f x)). apply path_contr. Defined.
Require Import HoTT.Basics HoTT.Types.