Denotational Semantics: The Scott-Strachey Approach to PL Theory, in Agda