I.T28 — Cartesian Closed

E_tau is cartesian closed: Hom(A x B, C) <-> Hom(A, C^B) pointwise. The evaluation morphism (Q^P x P) -> Q is verified. Internal hom with terminal/initial satisfies expected identities.