Since intersections are the products in $\mathcal{P}\webleft (X\webright )$ (Item 1 of Proposition 2.4.3.1.3), the left adjoint $\mathbf{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (U,V\webright )$ may be thought of as a function type $\webleft [U,V\webright ]$.
Then, under the Curry–Howard correspondence, the function type $\webleft [U,V\webright ]$ corresponds to implication $U\implies V$, which is logically equivalent to the statement $\neg U\vee V$. This in turn corresponds to the set $U^{\textsf{c}}\vee V=\webleft (X\setminus U\webright )\cup V$.
