Registry · Lemma VII.L26 tau-effective formalized

VII.L26 — Dignity Witness

Dignity functor D is well-defined; admissible subworld A_dig is closed under limits and internal homs.

Book VII Part 7 Ch. 76

Dependency Graph

Depends on (1)

VII.D65

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.dignity_witness