Cubical Agda is extended with Nakano’s later modality and guarded recursion based on Ticked Cubical Type Theory. (from Agda)

References:
Guarded Cubical