Registry · Definition I.D61 tau-effective formalized

I.D61 — Cartesian Monoidal Structure

The cartesian monoidal structure (E_tau, x, 1): unit is the terminal presheaf (all-true), tensor is pointwise conjunction. Left and right unit laws hold.

Book I Part 15 Ch. 57

Dependency Graph

Depends on (2)

I.D60 I.T26

Depended on by (1)

I.D63

Lean Formalization

Module: TauLib.BookI.Topos.CartesianProduct

Symbol: Tau.Topos.CartesianMonoidal