Theorems · Definition · category theory

CategoryTheory.GradedNatTrans.mk.noConfusion

{V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} →
        {inst_2 : CategoryTheory.EnrichedCategory V C} →
          {D : Type u₂} →
            {inst_3 : CategoryTheory.EnrichedCategory V D} →
              {A : CategoryTheory.Center V} →
                {F G : CategoryTheory.EnrichedFunctor V C D} →
                  {P : Sort u} →
                    {app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X} →
                      {naturality :
                          ∀ (X Y : C),
                            CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
                                  (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
                                (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))} →
                        {app' : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X} →
                          {naturality' :
                              ∀ (X Y : C),
                                CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app' Y))
                                      (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (app' X) (G.map X Y))
                                    (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))} →
                            { app := app, naturality := naturality } = { app := app', naturality := naturality' } →
                              (app ≍ app' → P) → P

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms