Definition lax_extension_laws {V : quantale_cosmos} {F : SET ⟶ SET} (L : lax_extension_data V F) : UU := (∏ (X Y : hSet) (R S : enriched_relation V X Y), R ≤e S → L _ _ R ≤e L _ _ S) × (∏ (X Y Z : hSet) (R : enriched_relation V X Y) (S : enriched_relation V Y Z), L _ _ R ·e L _ _ S ≤e L _ _ (R ·e S)) × (∏ (X Y : hSet) (f : X → Y), (#F f)^* ≤e L _ _ (f^*)) × (∏ (X Y : hSet) (f : X → Y), (#F f)^o ≤e L _ _ (f^o)).
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.