Proposition enriched_relation_square_to_le {X Y : hSet} {R₁ : enriched_relation V X Y} {R₂ : enriched_relation V X Y} (p : enriched_relation_square (idfun _) (idfun _) R₁ R₂) : R₁ ≤e R₂. Proof. exact p. 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.