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