Registry · Proposition I.P28 tau-effective formalized

I.P28 — Self-Enrichment

E_tau is self-enriched: internal hom gives an internal presheaf of morphisms. Every internal hom Q^P is itself a Presheaf.

Book I Part 15 Ch. 59

Dependency Graph

Depends on (2)

I.D64 I.T28

Lean Formalization

Module: TauLib.BookI.Topos.InternalHom

Symbol: Tau.Topos.self_enrichment