Proposition poset_category_weq_poset_right (P : Poset) : poset_category_to_poset (poset_to_poset_category P) = P. Proof. use total2_paths_f. - use total2_paths_f. + apply idpath. + apply isapropisaset. - use subtypePath. { intro. apply isaprop_isPartialOrder. } etrans. { apply (@pr1_transportf hSet hrel). } etrans. { apply transportf_total2_paths_f. } cbn. apply idpath. 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.