proposition: Proposition set_enrichment_laws : enrichment_laws set_enrichment_data.
proof: Proof. repeat split. - intros x y. use funextsec ; intro ; cbn. rewrite id_right. apply idpath. - intros x y. use funextsec ; intro ; cbn. rewrite id_left. apply idpath. - intros w x y z. use funextsec ; intro ; cbn. apply assoc. - intros x y f. use funextsec ; intro w ; cbn. apply maponpaths. apply isapropunit. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Examples.SetCartesianMonoidal