Proposition enriched_relation_le_comp {X Y Z : hSet} {R₁ R₂ : enriched_relation V X Y} {S₁ S₂ : enriched_relation V Y Z} (p : enriched_relation_le R₁ R₂) (q : enriched_relation_le S₁ S₂) : enriched_relation_le (R₁ ·e S₁) (R₂ ·e S₂). Proof. intros x z. use CoproductArrow. intros y ; cbn. exact ((p _ _ #⊗ q _ _) · CoproductIn _ _ _ y). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.PosetCat. Require Import UniMath.CategoryTheory.Limits.Coends. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.