Definition ob_eq_poset_category {C : poset_category} {x y : C} (f : x --> y) (g : y --> x) : x = y. Proof. use (isotoid C (univalent_category_is_univalent C)). exact (z_iso_poset_category f g). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.CategoryEquality.