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)

Depended on by (5)

Lean Formalization

Module: TauLib.BookII.Regularity.PreYoneda

Symbol: preyoneda_embed