fact: Definition nat_trans_with_set_enrichment_weq_nat_trans {C₁ C₂ : category} (F G : C₁ ⟶ C₂) : @nat_trans_with_enrichment _ (C₁ ,, set_enrichment C₁) (C₂ ,, set_enrichment C₂) (F ,, functor_set_enrichment F) (G ,, functor_set_enrichment G) ≃ F ⟹ G.
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