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)

I.D50 I.T20 I.P24

Depended on by (7)

I.D52 I.D55 I.D56 I.D83 I.P25 I.P29 I.T22

Lean Formalization

Module: TauLib.BookI.Topos.EarnedArrows

Symbol: Tau.Topos.CatTau