Theorems · Definition · category theory

CategoryTheory.AddMod.Hom.noConfusion

{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.MonoidalCategory C} →
        {D : Type u₂} →
          {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
            {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
              {A : C} →
                {inst_4 : CategoryTheory.AddMonObj A} →
                  {M N : CategoryTheory.AddMod D A} →
                    {t : M.Hom N} →
                      {C' : Type u₁} →
                        {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                          {inst'_1 : CategoryTheory.MonoidalCategory C'} →
                            {D' : Type u₂} →
                              {inst'_2 : CategoryTheory.Category.{v₂, u₂} D'} →
                                {inst'_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C' D'} →
                                  {A' : C'} →
                                    {inst'_4 : CategoryTheory.AddMonObj A'} →
                                      {M' N' : CategoryTheory.AddMod D' A'} →
                                        {t' : M'.Hom N'} →
                                          C = C' →
                                            inst ≍ inst' →
                                              inst_1 ≍ inst'_1 →
                                                D = D' →
                                                  inst_2 ≍ inst'_2 →
                                                    inst_3 ≍ inst'_3 →
                                                      A ≍ A' →
                                                        inst_4 ≍ inst'_4 →
                                                          M ≍ M' →
                                                            N ≍ N' →
                                                              t ≍ t' → CategoryTheory.AddMod.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Monoidal.Mod

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms