[Agda] How can I implement naive sized lambdas?

[Dr. ERDI Gergo]

On Sat, 4 Apr 2020, Georgi Lyubenov wrote:

> That said, is there some "well-scoped syntaxes 101" resource that I could read? The
> only particular thing I am aware of is "Everybody's Got To Be Somewhere" by Conor
> McBride.

There's A type and scope safe universe of syntaxes with binding : their 
semantics and proofs (https://strathprints.strath.ac.uk/64841/) and my own 
Generic Description of Well-Scoped, Well-Typed Syntaxes (https://arxiv.org/abs/1804.00119)