Registry · Proposition VII.P07 tau-effective formalized

VII.P07 — Special Composition Answer

Parts compose if and only if their diagram admits a colimit in the relevant category; dissolves the Special Composition Question.

Book VII Part 2 Ch. 27

Dependency Graph

Depends on (1)

VII.D35

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.special_composition_answer