Registry · Proposition I.P26 tau-effective formalized

I.P26 — Countable Topos

PSh(Cat_tau) is a countable topos: Cat_tau has countable objects and at most one morphism between each pair (thin). Presheaves are countably generated by functions TauIdx -> Bool.

Book I Part 14 Ch. 55

Dependency Graph

Depends on (2)

I.D57 I.P25

Lean Formalization

Module: TauLib.BookI.Topos.LimitsSites

Symbol: Tau.Topos.psh_countable_objects