Lemma antisymm_po_category_isweq (PO : po X) {A B : po_category PO} (poasymm : isantisymm PO) : isweq (λ p : A = B, idtoiso p). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.