Definition functor_with_lax_extension (V : quantale_cosmos) : UU := ∑ (F : SET ⟶ SET), lax_extension V F. Coercion functor_with_lax_extension_to_functor {V : quantale_cosmos} (F : functor_with_lax_extension V) : SET ⟶ SET. Proof. exact (pr1 F). Defined.
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.