proposition: Lemma antisymm_po_category_isweq (PO : po X) {A B : po_category PO} (poasymm : isantisymm PO) : isweq (λ p : A = B, idtoiso p).
proof: Proof. use isweq_iso. - apply (antisymm_po_category_isoiseq PO poasymm). - intro eq. apply proofirrelevance. apply xisaset. - intro iso. use z_iso_eq. apply proofirrelevance. apply propproperty. Defined.
imports: UniMath.Foundations.HLevels UniMath.Foundations.Sets UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence