A simple application of Yoneda argument is to prove that in Cartesian closed category.
Lemma. In Cartesian closed category, where is terminal.
Proof. for all objects . Hene .
It’s also quite easy to see that since . Hence . It’s just like that we prvoe the equality in the Heyting algebra!