Registry · Definition I.D54 tau-effective formalized

I.D54 — Yoneda Embedding

The Yoneda embedding y: Cat_tau -> PSh(Cat_tau) sends X to Hom(-, X). In thin Cat_tau, representable presheaves are subterminal (all hom-sets are singletons).

Book I Part 14 Ch. 54

Dependency Graph

Depends on (2)

I.D52 I.D53

Depended on by (4)

I.D57 I.D64 I.D83 I.T23

Lean Formalization

Module: TauLib.BookI.Topos.Functors

Symbol: Tau.Topos.yoneda