Theorems · Theorem · category theory

CategoryTheory.coyonedaPairingExt

∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)}
  {x y : (CategoryTheory.coyonedaPairing C).obj X}, (∀ (Y : C), x.app Y = y.app Y) → x = y

Defined in

Mathlib.CategoryTheory.Yoneda

Cited by

1 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category