There are tons, but we really need to ask if any of this is a fair topic for Dependent Typing, which has only emerged from pi-calculus musings on paper to compi

There are tons, but we really need to ask if any of this is a fair topic for Dependent Typing, which has only emerged from pi-calculus musings on paper to compilers that can do more than prove simple structural recursion. It's like seeing a photo of a baby and asking why there isn't a service to provide police records for babies, because you "just want to be careful, you know?"