I think Kind-Core should be that language. It is the simplest proof kernel, after all, by far :) And it has nothing human or inventive. Basically just the lambd

I think Kind-Core should be that language. It is the simplest proof kernel, after all, by far :) And it has nothing human or inventive. Basically just the lambda calculus with the self dependent function type. But I guess it ultimately is this old XKCD kind of problem: https://xkcd.com/927/ https://xkcd.com/927/