Lemma isapropsubtype {X : UU} (A : hsubtype X) (is : ∏ (x1 x2 : X), A x1 -> A x2 -> x1 = x2) : isaprop (carrier A). Proof. intros. apply invproofirrelevance. intros x x'. assert (X0 : isincl (@pr1 _ A)). { apply isinclpr1. intro x0. apply (pr2 (A x0)). } apply (invmaponpathsincl (@pr1 _ A) X0). induction x as [ x0 is0 ]. induction x' as [ x0' is0' ]. simpl. apply (is x0 x0' is0 is0'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.