Registry · Theorem I.T25 tau-effective formalized

I.T25 — Omega_tau Subobject Classifier

Omega_tau = Truth4 is the subobject classifier for PSh(Cat_tau). Every truth value is one of T, F, B, N. The four elements are pairwise distinct (omega_tau_card_four). Previewed in Part XI, now EARNED.

Book I Part 14 Ch. 56

Dependency Graph

Depends on (3)

I.D41 I.D57 I.T24

Depended on by (2)

I.D58 I.D59

Lean Formalization

Module: TauLib.BookI.Topos.EarnedTopos

Symbol: Tau.Topos.omega_tau_classifier