Registry · Definition I.D57 tau-effective formalized

I.D57 — Presheaf Topos

PSh(Cat_tau): the presheaf topos. A presheaf assigns to each object a set (modeled as a predicate). Includes terminal/initial presheaves and pointwise product/coproduct operations.

Book I Part 14 Ch. 55

Dependency Graph

Depends on (3)

I.D54 I.D55 I.D56

Depended on by (6)

I.D59 I.D60 I.D62 I.P26 I.T24 I.T25

Lean Formalization

Module: TauLib.BookI.Topos.LimitsSites

Symbol: Tau.Topos.PShCatTau