Definition poset_to_precategory_data : precategory_data. Proof. use make_precategory_data. - use make_precategory_ob_mor. + exact P. + exact (λ x y, x ≤ y)%poset. - use isrefl_posetRelation. - use istrans_posetRelation. 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.