Proposition enriched_relation_rinvunitor {X Y : hSet} (R : enriched_relation V X Y) : enriched_relation_square (idfun _) (idfun _) R (R ·e id_enriched_relation _). Proof. intros x y ; cbn. refine (_ · CoproductIn _ _ _ y). refine (mon_rinvunitor _ · _). refine (identity _ #⊗ _). exact (CoproductIn _ _ _ (idpath 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.