Proposition lax_extension_companion_left {V : quantale_cosmos} {F : SET ⟶ SET} (L : lax_extension V F) {X Y Z : hSet} (f : X → Y) (R : enriched_relation V Y Z) : L _ _ (f^* ·e R) = (#F f)^* ·e L _ _ R. Proof. use eq_enriched_relation_le. - refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_linvunitor. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). exact (comp_companion_conjoint_enriched_relation (#F f)). } refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_lassociator. } refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). apply (lax_extension_enriched_rel_conjoint L). } refine (enriched_relation_le_trans _ _). { apply lax_extension_enriched_rel_comp. } use lax_extension_enriched_rel_le. refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_rassociator. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). apply comp_conjoint_companion_enriched_relation. } use enriched_relation_square_to_le. apply enriched_relation_lunitor. - intros x z. refine (_ · lax_extension_enriched_rel_comp _ _ _ _ _). use enriched_relation_le_comp. + apply lax_extension_enriched_rel_companion. + apply enriched_relation_le_refl. 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.