Guarded Cubical¶
Note
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.
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.