Proposition is_univalent_poset_to_category : is_univalent poset_to_category. Proof. intros x y. use isweqimplimpl. - intro f. use isantisymm_posetRelation. + apply f. + exact (inv_from_z_iso f). - apply setproperty. - use isaproptotal2. + intro. apply isaprop_is_z_isomorphism. + intros. apply propproperty. Qed.
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.