Registry · Theorem VII.T31 tau-effective formalized

VII.T31 — CI-Sheaf Equivalence

The categorical imperative is formally equivalent to the sheaf condition; universalizability IS gluing; Kant formalized.

Book VII Part 7 Ch. 77

Dependency Graph

Depends on (2)

VII.D66 VII.T30

Depended on by (8)

VII.L12 VII.L27 VII.L40 VII.P17 VII.P18 VII.P25 VII.T32 VII.T35

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.ci_sheaf_equivalence