David Corfield reader monad

Given type $A$ and type of interpreters $I$, then $A^I$ contains as elements assignments of $a(i): A$ for $i:I$. E.g., $i$‘s favourite colour.

But $A$ could be $Type$ or $Prop$, then $Prop^I$ would have elements such as ‘$i$ believes that $P$’.