Definition poset_category_to_poset (C : poset_category) : Poset. Proof. use make_Poset. - use make_hSet. + exact C. + exact (isaset_ob_poset C). - use make_PartialOrder. + refine (λ x y, make_hProp (x --> y) _). apply is_poset_poset_category. + repeat split. * abstract (intros x y z f g ; cbn in * ; exact (f · g)). * abstract (intro x ; cbn in * ; apply identity). * abstract (intros x y f g ; cbn in * ; exact (ob_eq_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.