Proposition set_enrichment_laws : enrichment_laws set_enrichment_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Examples.SetCartesianMonoidal. Import MonoidalNotations.