Theorems · Definition · category theory

CategoryTheory.InducedCategory.Hom.noConfusion

{P : Sort u} →
  {C : Type u₁} →
    {D : Type u₂} →
      {inst : CategoryTheory.Category.{v, u₂} D} →
        {F : C → D} →
          {X Y : CategoryTheory.InducedCategory D F} →
            {t : X.Hom Y} →
              {C' : Type u₁} →
                {D' : Type u₂} →
                  {inst' : CategoryTheory.Category.{v, u₂} D'} →
                    {F' : C' → D'} →
                      {X' Y' : CategoryTheory.InducedCategory D' F'} →
                        {t' : X'.Hom Y'} →
                          C = C' →
                            D = D' →
                              inst ≍ inst' →
                                F ≍ F' →
                                  X ≍ X' → Y ≍ Y' → t ≍ t' → CategoryTheory.InducedCategory.Hom.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms