## Propositions As Types : 1

One of my favorite tricks — it seems almost too tricky to be true — is the Propositions As Types Analogy. And I seem to see hints that the 2-part analogy can be extended to a 3-part analogy, as follows.

$\text{proof hint : proof : proposition ~::~ untyped term : typed term : type}$

See my working notes on Propositions As Types for more information.