Definition eq_nat_trans_with_enrichment {V : monoidal_cat} {E₁ : cat_with_enrichment V} {E₂ : cat_with_enrichment V} {F : functor_with_enrichment E₁ E₂} {G : functor_with_enrichment E₁ E₂} {τ₁ τ₂ : nat_trans_with_enrichment F G} (p : ∏ (x : E₁), pr1 τ₁ x = pr1 τ₂ x) : τ₁ = τ₂.
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.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.whiskering.