Registry · Definition VII.D35 tau-effective formalized

VII.D35 — Mereological Composition as Colimit

Whole is colimit of parts; composition occurs when colimit exists in admissible category.

Book VII Part 2 Ch. 27

Dependency Graph

Depended on by (1)

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.MereologicalCompositionAsColimit