Registry · Definition I.D62 tau-effective formalized

I.D62 — Categorical Coproduct

The categorical coproduct (wedge product) of two presheaves: pointwise disjunction. P v Q maps each object X to P(X) OR Q(X). Injections embed each factor.

Book I Part 15 Ch. 58

Dependency Graph

Depends on (1)

I.D57

Depended on by (2)

I.D63 I.T27

Lean Formalization

Module: TauLib.BookI.Topos.WedgeProduct

Symbol: Tau.Topos.cat_coproduct