Registry · Definition I.D60 tau-effective formalized

I.D60 — Categorical Product

The categorical product of two presheaves: pointwise conjunction of support predicates. P x Q maps each object X to P(X) AND Q(X). Projections extract each factor.

Book I Part 15 Ch. 57

Dependency Graph

Depends on (2)

I.D55 I.D57

Depended on by (5)

I.D61 I.D64 I.T26 I.T27 I.T28

Lean Formalization

Module: TauLib.BookI.Topos.CartesianProduct

Symbol: Tau.Topos.cat_product