Proposition comp_companion_conjoint_enriched_relation {X Y : hSet} (f : X → Y) : enriched_relation_le (id_enriched_relation _) (f^* ·e f^o). Proof. intros x x'. use CoproductArrow. intro p ; induction p ; cbn. refine (_ · CoproductIn _ _ _ (f x)). refine (_ · (CoproductIn _ _ _ (idpath _) #⊗ CoproductIn _ _ _ (idpath _))). 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.