~ (IsHSet Type). Proof. intro HT. apply true_ne_false. pose (r := path_ishprop (path_universe equiv_negb) 1). refine (_ @ (ap (fun q => transport idmap q false) r)). symmetry; apply transport_path_universe. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.