Registry · Definition I.D50 tau-effective formalized

I.D50 — Tau-Arrow

A tau-arrow from source to target is a HolFun (tau-holomorphic function). Two arrows are equal iff their underlying HolFuns agree extensionally at all inputs and stages.

Book I Part 14 Ch. 53

Dependency Graph

Depends on (2)

I.D47 I.T21

Depended on by (1)

I.D51

Lean Formalization

Module: TauLib.BookI.Topos.EarnedArrows

Symbol: Tau.Topos.TauArrow