Registry · Definition I.D51 tau-effective formalized

I.D51 — Cat_tau

Cat_tau: the earned category with objects = TauIdx, morphisms = tau-arrows. Identity from id_holfun, composition from HolFun composition, associativity from Part XII. Not imported but EARNED from the monoid structure.

Book I Part 14 Ch. 53

Dependency Graph

Depends on (3)

Depended on by (7)

Lean Formalization

Module: TauLib.BookI.Topos.EarnedArrows

Symbol: Tau.Topos.CatTau