Definition enrichment_over_poset_weq_poset_enrichment_inv_iso (x y : C) : z_iso ((pr11 (make_enrichment_over_poset C (make_poset_enrichment C E))) x y) (E ⦃ x , y ⦄). Proof. use make_z_iso ; cbn. - simple refine (_ ,, _). + exact (λ f, pr1 (enriched_from_arr E f) tt). + abstract (cbn ; intros f g p ; apply p). - simple refine (_ ,, _). + refine (λ f, enriched_to_arr E _). simple refine (_ ,, _). * exact (λ _, f). * abstract (cbn ; intros t₁ t₂ p ; apply refl_PartialOrder). + abstract (intros f₁ f₂ p ; cbn ; rewrite !enriched_from_to_arr ; cbn ; exact p). - split. + abstract (use eq_monotone_function ; intro f ; cbn in * ; refine (_ @ enriched_to_from_arr E f) ; apply maponpaths ; use eq_monotone_function ; intro t ; cbn ; apply maponpaths ; apply isapropunit). + abstract (use eq_monotone_function ; intro f ; cbn in * ; assert (is_monotone unit_PartialOrder (pr2 (E ⦃ x, y ⦄)) (λ _ : unit, f)) as H ; [ intros t₁ t₂ p ; apply refl_PartialOrder | ] ; refine (_ @ eqtohomot (maponpaths pr1 (enriched_from_to_arr E (_ ,, H))) tt) ; cbn ; apply maponpaths_2 ; do 3 apply maponpaths ; apply isaprop_is_monotone). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Examples.PosetsMonoidal. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Section FromPosetEnrichment. End FromPosetEnrichment.