Definition enrichment_over_poset_weq_poset_enrichment_inv_1 : make_enrichment_over_poset C (make_poset_enrichment C E) = E. Proof. use subtypePath. { intro. apply isaprop_enrichment_laws. } use (invweq (total2_paths_equiv _ _ _)). use (invmap (enrichment_data_hom_path _ _ _)). { exact is_univalent_category_of_posets. } simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact enrichment_over_poset_weq_poset_enrichment_inv_iso. - abstract (intro x ; use eq_monotone_function ; intro w ; cbn ; rewrite enriched_from_arr_id ; apply maponpaths ; apply isapropunit). - abstract (intros x y z ; use eq_monotone_function ; intro w ; cbn ; rewrite enriched_from_arr_comp ; cbn ; apply idpath). - abstract (intros x y f ; use eq_monotone_function ; intro w ; cbn ; apply maponpaths ; apply isapropunit). - abstract (intros x y f ; cbn ; refine (!_) ; refine (_ @ enriched_to_from_arr E (pr1 f tt)) ; apply maponpaths ; use eq_monotone_function ; intro w ; cbn ; induction w ; apply idpath). 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.