Explaining my encoding of a HOAS datatype, part 1

I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.  The goal is to encode a datatype (including its constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submit is the simplest higher-order datatype possible.  I just explain some of the setup, and will attempt wading through the details next time.