`{Funext} (e : Bool <~> Bool) : (e = equiv_idmap Bool) + (e = equiv_negb). Proof. revert e. equiv_intro equiv_bool_aut_bool e. destruct e; simpl. - exact (inl idpath). - exact (inr idpath). Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.