Proposition companion_enriched_relation_comp {X Y Z : hSet} (f : X → Y) (g : Y → Z) : (λ x, g(f x))^* ≤e f^* ·e g^*. Proof. intros x z. use CoproductArrow ; cbn. intro p. refine (_ · CoproductIn _ _ _ (f x)). refine (_ · (CoproductIn _ _ _ (idpath _) #⊗ CoproductIn _ _ _ p)). apply mon_linvunitor. 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.