ishset_N@{} : IsHSet N. Proof. apply istrunc_S. intros n m. change (IsHProp (n = m)). refine (istrunc_equiv_istrunc (n.1 = m.1) (equiv_path_sigma_hprop n m)). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.