Registry · Definition II.D50 established formalized

II.D50 — Pre-Yoneda Embedding

Pre-Yoneda Embedding

Book II Part 7 Ch. 40

Dependency Graph

Depends on (5)

I.T40 II.D37 II.D47 II.T27 II.L07

Depended on by (5)

II.D53 II.L11 II.L14 II.P10 II.R12

Lean Formalization

Module: TauLib.BookII.Regularity.PreYoneda

Symbol: preyoneda_embed