Definition nat_trans_from_empty_enrichment {C : category} {E : enrichment C V} {F G : empty_category ⟶ C} (FE : functor_enrichment F empty_category_enrichment E) (GE : functor_enrichment G empty_category_enrichment E) : nat_trans_enrichment (nat_trans_from_empty F G) FE GE.
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.StandardCategories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.Monoidal.Categories.