Theorems · Theorem · category theory

CategoryTheory.NatTrans.ext

∀ {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 y : CategoryTheory.NatTrans F G}, x.app = y.app → x = y

Defined in

Mathlib.CategoryTheory.NatTrans

Cited by

20 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms