Guarded Cubical


This is a stub.

Cubical Agda is extended with Nakano’s later modality and guarded recursion based on Ticked Cubical Type Theory [2]. For its usage, see [1] or the example.


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