Start / Iowa Type Theory Commute / Explaining my encoding of a hoas datatype part 1

Explaining my encoding of a HOAS datatype, part 1

10 min • 19 oktober 2020

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.