Henning Makholm suggests the following heuristic intuition for the internal Hom of $\mathcal{P}\webleft (X\webright )$ from $U$ to $V$ ([MSE 267365]):
- Since products in $\mathcal{P}\webleft (X\webright )$ are given by binary intersections (Item 1 of Proposition 2.4.1.1.4), the right adjoint $\mathbf{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (U,-\webright )$ of $U\cap -$ may be thought of as a function type $\webleft [U,V\webright ]$.
-
Under the Curry–Howard correspondence (
), the function type $\webleft [U,V\webright ]$ corresponds to implication $U\Longrightarrow V$.
- Implication $U\Rightarrow V$ is logically equivalent to $\neg U\vee V$.
- The expression $\neg U\vee V$ then corresponds to the set $U^{\textsf{c}}\cup V$ in $\mathcal{P}\webleft (X\webright )$.
- The set $U^{\textsf{c}}\vee V$ turns out to indeed be the internal Hom of $\mathcal{P}\webleft (X\webright )$.
