Proposition isaprop_lax_extension_laws {V : quantale_cosmos} {F : SET ⟶ SET} (L : lax_extension_data V F) : isaprop (lax_extension_laws L). Proof. repeat (use isapropdirprod) ; repeat (use impred ; intro) ; apply is_poset_category_quantale_cosmos. 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.