redtt
redtt copied to clipboard
Typechecking for regular types
Do we have a good proof theory for them? @cangiuli @mortberg
Do you mean, types satisfying regularity? I thought we didn't think this was a useful kind.
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.
Ah, I see. I have never thought seriously about their proof theory, and I don't think @mortberg has either?
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.