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.”