Registry · Definition II.D54 established formalized

II.D54 — Hom Object

The internal Hom object as the inverse limit of stage-k morphism sets. A tau-object with NF address, bipolar decomposition, and tower coherence.

Book II Part 8 Ch. 42

Dependency Graph

Depends on (5)

I.D20 I.D21 I.T05 II.D49 II.L07

Depended on by (11)

II.D55 II.D56 II.D57 II.D58 II.L11 II.P11 II.P12 II.P21 II.R14 II.R15 II.T36

Lean Formalization

Module: TauLib.BookII.Enrichment.SelfEnrichment

Symbol: Tau.BookII.Enrichment.hom_obj_count_affine