Registry · Definition I.D64 tau-effective formalized

I.D64 — Internal Hom

The internal hom Q^P: pointwise Boolean implication. (Q^P)(X) = true iff P(X) implies Q(X). This gives exponentials in E_tau.

Book I Part 15 Ch. 59

Dependency Graph

Depends on (2)

I.D60 I.D54

Depended on by (2)

I.P28 I.T28

Lean Formalization

Module: TauLib.BookI.Topos.InternalHom

Symbol: Tau.Topos.internal_hom