Theorem iscontr_set_enrichment : iscontr (enrichment C SET_monoidal_cat). 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.
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.