Registry · Definition VII.D62 tau-effective formalized

VII.D62 — Modal Frame in τ

Possible worlds as internal objects with accessibility morphisms; Kripke frames as special case of presheaf structure.

Book VII Part 6 Ch. 73

Dependency Graph

Depended on by (2)

VII.L09 VII.T28

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.ModalFrameTau