(H : forall P, IsHProp P -> {Q : Type & P <-> ~Q}) : DNE_type. Proof. intros P ? nnp. destruct (H P _) as [Q e]. apply e. intros q. apply nnp. intros p. exact (fst e p q). Defined.
Require Import HoTT.Basics HoTT.Types.