`{Funext} : (forall b, P b) <~> P false * P true. Proof. apply (equiv_adjointify f g); repeat (reflexivity || intros [] || intro || apply path_forall). Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.