use module system of agda example semantics for simply typed lambda calculus how to handle dual construction? create agda library file