Proposition lax_extension_enriched_relation_square {V : quantale_cosmos} {F : SET ⟶ SET} (L : lax_extension V F) {X₁ X₂ Y₁ Y₂ : hSet} {R : enriched_relation V X₁ Y₁} {S : enriched_relation V X₂ Y₂} {f : X₁ → X₂} {g : Y₁ → Y₂} (p : enriched_relation_square f g R S) : enriched_relation_square (# F f) (# F g) (L X₁ Y₁ R) (L X₂ Y₂ S). Proof. unfold enriched_relation_square in *. rewrite <- enriched_relation_comp_conj. rewrite <- lax_extension_conjoint_right. rewrite <- lax_extension_companion_left. apply lax_extension_enriched_rel_le. rewrite enriched_relation_comp_conj. apply p. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichedRelation. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import MonoidalNotations.