Registry · Lemma II.L11 established formalized

II.L11 — Probe Naturality iff Yoneda

Probe Naturality iff Yoneda

Book II Part 8 Ch. 43

Dependency Graph

Depends on (5)

II.D50 II.R12 II.T33 II.D53 II.D54

Depended on by (1)

II.T36

Lean Formalization

Module: TauLib.BookII.Enrichment.YonedaTheorem

Symbol: Tau.BookII.Enrichment.probe_yoneda_check