Theorems · Definition · category theory

CategoryTheory.Comon.Hom.noConfusion

{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.MonoidalCategory C} →
        {M N : CategoryTheory.Comon C} →
          {t : M.Hom N} →
            {C' : Type u₁} →
              {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                {inst'_1 : CategoryTheory.MonoidalCategory C'} →
                  {M' N' : CategoryTheory.Comon C'} →
                    {t' : M'.Hom N'} →
                      C = C' →
                        inst ≍ inst' →
                          inst_1 ≍ inst'_1 → M ≍ M' → N ≍ N' → t ≍ t' → CategoryTheory.Comon.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Monoidal.Comon_

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms