Theorems · Definition · category theory

CategoryTheory.Comon.Hom.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {M N : CategoryTheory.Comon C} →
        {P : Sort u} →
          {hom : M.X ⟶ N.X} →
            {isComonHom_hom : CategoryTheory.IsComonHom hom} →
              {hom' : M.X ⟶ N.X} →
                {isComonHom_hom' : CategoryTheory.IsComonHom hom'} →
                  { hom := hom, isComonHom_hom := isComonHom_hom } =
                      { hom := hom', isComonHom_hom := isComonHom_hom' } →
                    (hom ≍ hom' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.Comon_

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms