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. Proof. use weq_iso. - exact (λ τ, pr1 τ ,, is_nat_trans_from_enrichment (pr2 τ)). - exact (λ τ, pr1 τ ,, nat_trans_set_enrichment τ). - abstract (intro τ ; use eq_nat_trans_with_enrichment ; intro x ; cbn ; apply idpath). - abstract (intro τ ; use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; apply idpath). Defined.
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.