Lemma antisymm_po_category_isoiseq (PO : po X) {A B : (po_category PO)} (poasymm : isantisymm PO) (isoAB : z_iso A B) : A = B. Proof. unfold isantisymm in *. apply poasymm. apply (z_iso_mor isoAB). apply (inv_from_z_iso isoAB). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.