`{Funext} (P : Type) : P * P <~> (Bool -> P) := (equiv_bool_forall_prod (fun _ => P))^-1%equiv. Global Instance isequiv_negb : IsEquiv negb. Proof. refine (@Build_IsEquiv _ _ negb negb (fun b => if b as b return negb (negb b) = b then idpath else idpath) (fun b => if b as b return negb (negb b) = b then idpath else idpath) _). intros []; simpl; exact idpath. Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.