Theorems · Theorem · category theory

CategoryTheory.Functor.hext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D},
  (∀ (X : C), F.obj X = G.obj X) → (∀ (X Y : C) (f : X ⟶ Y), F.map f ≍ G.map f) → F = G

Proving equality between functors using heterogeneous equality.

Defined in

Mathlib.CategoryTheory.EqToHom

Cited by

15 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category