The trace comonad G is a comonad on the Heyting algebra H that preserves the Heyting structure — meets, joins, implication, and the bounded lattice operations.
A comonad on H consists of:
- An endofunctor G: H → H
- A counit ε: G → id (extraction: every traced element can be “read off” to recover its base value)
- A comultiplication δ: G → G∘G (duplication: tracing can be iterated coherently)
satisfying coassociativity (δ composed with Gδ equals δ composed with δG) and the counit laws (εG ∘ δ = id = Gε ∘ δ).
What distinguishes the trace comonad from an arbitrary comonad on H is that G preserves all Heyting operations:
- G(a ∧ b) = G(a) ∧ G(b) (trace distributes over meet)
- G(a ∨ b) = G(a) ∨ G(b) (trace distributes over join)
- G(a → b) = G(a) → G(b) (trace distributes over implication)
This preservation means that tracing does not distort the logical structure. The traced version of a conjunction is the conjunction of the traces; the traced version of an implication is the implication of the traces.
In the semiotic universe, the trace comonad provides the mechanism by which signs carry their interpretive history. The counit extracts the current value; the comultiplication records that the tracing itself has been traced — enabling the self-referential structure that semiotic interpretation requires.