Registry · Theorem I.T26 tau-effective formalized

I.T26 — Product Universal Property

Product universal property: if R maps to both P and Q pointwise, then R maps to P x Q. Also: product is commutative, associative, and unital (with terminal presheaf).

Book I Part 15 Ch. 57

Dependency Graph

Depends on (1)

I.D60

Depended on by (2)

I.D61 I.T28

Lean Formalization

Module: TauLib.BookI.Topos.CartesianProduct

Symbol: Tau.Topos.product_universal