Guarded Type Theory¶
This is a stub.
--guarded extends Agda with
Nakano’s later modality and guarded recursion
based on Ticked (Cubical) Type Theory .
For its usage in combination with
--cubical, see  or the
The implementation currently allows for something more general than in the above reference, in preparation for the ticks described in .
Given a type
A in the
primLockUniv universe we can form function
types annotated with
@tick (or its synonym
(@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
only exception to that restriction, at the moment, are variables of
IsOne _ type.
 Niccolò Veltri and Andrea Vezzosi. “Formalizing pi-calculus in guarded cubical Agda.” In CPP’20. ACM, New York, NY, USA, 2020.
 Rasmus Ejlers Møgelberg and Niccolò Veltri. “Bisimulation as path type for guarded recursive types.” In POPL’19, 2019.
 Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi. “Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks.”