proposition: Lemma isdecproppathstoisolated (X : UU) (x : X) (is : isisolated X x) (x' : X) : isdecprop (x' = x).
proof: Proof. intros. apply (isdecpropweqf (weqpathsinv0 x x') (isdecproppathsfromisolated X x is x')). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom