Registry · Lemma VII.L39 tau-effective formalized

VII.L39 — Power Morphism Well-Typed

Power relation P : A → B is a valid morphism: asymmetry, scope, modality are structural categorical vocabulary.

Book VII Part 8 Ch. 104

Dependency Graph

Depends on (1)

VII.D80

Lean Formalization

Module: TauLib.BookVII.Social.Ontology

Symbol: Tau.BookVII.Social.Ontology.power_morphism_well_typed