Definition comp_h_enriched_relation_square {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : hSet} {f : X₁ → X₂} {g : Y₁ → Y₂} {h : Z₁ → Z₂} {R₁ : enriched_relation V X₁ Y₁} {S₁ : enriched_relation V Y₁ Z₁} {R₂ : enriched_relation V X₂ Y₂} {S₂ : enriched_relation V Y₂ Z₂} (τ : enriched_relation_square f g R₁ R₂) (θ : enriched_relation_square g h S₁ S₂) : enriched_relation_square f h (R₁ ·e S₁) (R₂ ·e S₂).
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.