Later Modality

[jonsterling]

In connection with what we're doing here at Aarhus, I want to start integrating guarded features with this language; this is a good example of where we'd want user-configurable flags as in RedPRL/algaett#23.

I think the first thing that we basically know how to do, using the ideas of Ranald and his collaborators, is add the Later modality. The result should look kind of like a cross between the stuff in the Clocked Type Theory/CloTT paper and the stuff in the dependent right adjoints paper.

[jonsterling]

I believe I now know enough to begin experimental implementation of this. No promises on correctness, but if it works at all, it probably must work in the way I am imagining right now.