Cubical Agda is extended with Nakano’s later modality and guarded recursion based on Ticked Cubical Type Theory. (from Agda)
References:
Guarded Cubical
Stats
|
created |
2 years, 6 months ago |
|
viewed |
4 times |
|
active |
2 years, 6 months ago |
|
editors |
1 |
Top Answerers
more »
Recent Hot Answers
Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?Is there a formalism of "coinductive" data types with negative occurrences?
How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?
Is there a formalism of "coinductive" data types with negative occurrences?
more »