All Questions
Tagged with agda guarded-recursion
2
questions
6
votes
2
answers
236
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
8
votes
1
answer
158
views
Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?
In Guarded Cubical Agda there's ▹_ : Set i → Set i and ▸_ : ▹ Set i → Set i.
If I've got ...
- 971