Registry · Lemma II.L14 established formalized

II.L14 — Yoneda Application

The Yoneda bijection identifies natural transformations with omega-germ transformers via a tower-coherent family of stage-k components.

Book II Part 9 Ch. 50

Dependency Graph

Depends on (5)

II.T35 II.L13 II.R12 II.D50 II.P10

Depended on by (2)

II.T39 II.T40

Lean Formalization

Module: TauLib.BookII.CentralTheorem.YonedaApplied

Symbol: Tau.BookII.CentralTheorem.yoneda_application_check