proposition: Theorem iscontr_set_enrichment : iscontr (enrichment C SET_monoidal_cat).
proof: Proof. refine (set_enrichment ,, _). intro E. use subtypePath. { intro. apply isaprop_enrichment_laws. } use (invweq (total2_paths_equiv _ _ _)). use (invmap (enrichment_data_hom_path _ (pr1 E) set_enrichment_data)). { exact is_univalent_HSET. } simple refine (_ ,, _ ,, _ ,, _ ,, _). - intros x y. use make_z_iso. + exact (λ f, enriched_to_arr E (λ _, f)). + exact (λ f, enriched_from_arr E f tt). + split. * use funextsec ; intro f ; cbn. rewrite enriched_from_to_arr. apply idpath. * use funextsec ; intro f ; cbn. refine (_ @ enriched_to_from_arr E _). apply maponpaths. use funextsec. intro z. apply maponpaths. apply isapropunit. - intro x ; use funextsec ; intro f ; cbn. refine (_ @ enriched_to_arr_id E _). apply maponpaths. use funextsec. intro z. apply maponpaths. apply isapropunit. - intros x y z ; use funextsec ; intro f ; cbn. use (invmaponpathsweq (invweq (_ ,, isweq_enriched_to_arr E _ _))) ; cbn. rewrite enriched_from_arr_comp ; cbn. rewrite !enriched_from_to_arr. apply idpath. - intros x y f ; use funextsec ; intro w ; cbn. refine (_ @ enriched_to_from_arr E _). apply maponpaths. use funextsec. intro z. apply maponpaths. apply isapropunit. - intros x y f ; cbn. apply maponpaths. use funextsec. intro z. 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