Definition poset_enrichment_binary_coprod_is_coprod : is_binary_coprod_enriched E' x y make_poset_enriched_binary_coprod_cocone. Proof. use make_is_binary_coprod_enriched. - intros z P f g. refine (_ · poset_enrichment_binary_coprod_pair _ _ _ _). simple refine (_ ,, _). + exact (prodtofuntoprod (pr1 f ,, pr1 g)). + apply prodtofun_is_monotone. * exact (pr2 f). * exact (pr2 g). - abstract (intros z P f g ; use eq_monotone_function ; intros w ; cbn ; apply poset_enrichment_obj_in1_sum). - abstract (intros z P f g ; use eq_monotone_function ; intros w ; cbn ; apply poset_enrichment_obj_in2_sum). - abstract (intros z P φ₁ φ₂ q₁ q₂ ; use eq_monotone_function ; intro w ; use poset_enrichment_binary_coprod_arr_eq ; [ exact (eqtohomot (maponpaths (λ f, pr1 f) q₁) w) | exact (eqtohomot (maponpaths (λ f, pr1 f) q₂) w) ]). 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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.PosetEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Examples.PosetsMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Import MonoidalNotations.