Guarded Type Theory

Note

This is a stub.

Option --guarded extends Agda with Nakano’s later modality and guarded recursion based on Ticked (Cubical) Type Theory [2]. For its usage in combination with --cubical, see [1] or the example.

The implementation currently allows for something more general than in the above reference, in preparation for the ticks described in [3].

Given a type A in the primLockUniv universe we can form function types annotated with @tick (or its synonym @lock): (@tick x : A) -> B. Lambda abstraction at such a type introduces the variable in the context with a @tick annotation. Application t u for t : (@tick x : A) → B is restricted so that t is typable in the prefix of the context that does not include any @tick variables in u. The only exception to that restriction, at the moment, are variables of interval I, or IsOne _ type.

References

[1] Niccolò Veltri and Andrea Vezzosi. “Formalizing pi-calculus in guarded cubical Agda.” In CPP’20. ACM, New York, NY, USA, 2020.

[2] Rasmus Ejlers Møgelberg and Niccolò Veltri. “Bisimulation as path type for guarded recursive types.” In POPL’19, 2019.

[3] Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi. “Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks.”