Theorems · Theorem · category theory

CategoryTheory.conj_eqToHom_iff_heq

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y)
  (h' : X = Z),
  f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)) ↔
    f ≍ g

Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal. Note this used to be in the Functor namespace, where it doesn't belong.

Defined in

Mathlib.CategoryTheory.EqToHom

Cited by

5 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

CategoryTheory.Category