This is a stub.
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 @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.
 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.”