Semantics of Simply Typed Lambda Calculus in Agda