Lemma isasetifiscontrloops (X : UU) : (∏ x : X, iscontr (x = x)) -> isaset X. Proof. intros X0. unfold isaset. unfold isofhlevel. intros x x' x0 x0'. induction x0. apply isapropifcontr. exact (X0 x). Defined.