Proposition eq_lax_extension {V : quantale_cosmos} {F : SET ⟶ SET} {L L' : lax_extension V F} (p : ∏ (X Y : hSet) (R : enriched_relation V X Y), L X Y R = L' X Y R) : L = L'. Proof. use subtypePath. { intro. apply isaprop_lax_extension_laws. } use funextsec ; intro X. use funextsec ; intro Y. use funextsec ; intro R. exact (p X Y R). 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.