New answers tagged

1

You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type). I couldn't find the reference I was thinking of right now, but a quick search for "agda hereditary subtitutions STLC" pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/...


3

Take any small symmetric monoidal category $V$. Then the category of $V$-valued presheaves will (a) have closed monoidal structure (via Day convolution), and (b) have enough stuff (inherited from $\mathrm{Set}$) to interpret dependent types. This gives you enough structure to interpret something like our LNL calculus pretty easily, because there is a nice ...


Top 50 recent answers are included