Theorems · Definition · category theory

CategoryTheory.CommRingObjCat.Hom.noConfusion

{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
        {inst_2 : CategoryTheory.BraidedCategory C} →
          {R₁ R₂ : CategoryTheory.CommRingObjCat C} →
            {t : R₁.Hom R₂} →
              {C' : Type u} →
                {inst' : CategoryTheory.Category.{v, u} C'} →
                  {inst'_1 : CategoryTheory.CartesianMonoidalCategory C'} →
                    {inst'_2 : CategoryTheory.BraidedCategory C'} →
                      {R₁' R₂' : CategoryTheory.CommRingObjCat C'} →
                        {t' : R₁'.Hom R₂'} →
                          C = C' →
                            inst ≍ inst' →
                              inst_1 ≍ inst'_1 →
                                inst_2 ≍ inst'_2 →
                                  R₁ ≍ R₁' →
                                    R₂ ≍ R₂' → t ≍ t' → CategoryTheory.CommRingObjCat.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms