Registry · Theorem
I.T22
tau-effective
formalized
I.T22 — Category Axioms
Cat_tau satisfies the category axioms: left/right identity for stagewise composition (id_stage), and associativity of composition (stagefun_comp_assoc). All proven from HolFun monoid properties.