Definition enriched_nat_trans_law {A B : enriched_precat} {F G : enriched_functor A B} (a : enriched_nat_trans_data F G) := ∏ (x y : A), enriched_functor_on_morphisms F x y · postcompose_underlying_morphism _ (a y) = enriched_functor_on_morphisms G x y · precompose_underlying_morphism _ (a x).
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Core.Isos. Import MonoidalNotations.