Kind systems

[favonia]

Do we have a good proof theory for them? @cangiuli @mortberg

[cangiuli]

Do you mean, types satisfying regularity? I thought we didn't think this was a useful kind.

[favonia]

We thought they were useless in the presence of discrete types, but now without equality types (in this proof theory) discrete types seem useless. So, maybe there is room for us to reconsider regular types.

[cangiuli]

Ah, I see. I have never thought seriously about their proof theory, and I don't think @mortberg has either?

[mortberg]

I have not, it would be interesting to have this though. I think some examples can be done in the regular fragment which should be more efficient.

[favonia]

It is unclear whether we want regular types, but we need to have a kind system first.