Registry · Definition II.D40 established formalized

II.D40 — Identity Map

The identity omega-germ transformer on a tau-admissible point x, defined by the identity map at each stage. The unit morphism in HolEnd(tau).

Book II Part 6 Ch. 33

Dependency Graph

Depends on (2)

I.D49 II.D39

Depended on by (2)

II.D41 II.T29

Lean Formalization

Module: TauLib.BookII.Hartogs.CategoryStructure

Symbol: hol_identity