[Agda] Initial Algebra Semantics for Lambda Calculus

[Martín]

Hello everyone,

I am looking for previous work done on Initial Algebra Semantics for 
Lambda Calculus (or STLC) in Agda, or anything related to continue 
working on it. My research is based on Initial Algebra Semantics and I 
wanted a good rich language to play on which has some recursive notion.

Any help is welcome, and thank you!

Martin.