All Questions
Tagged with agda coinductive-type
4
questions
6
votes
2
answers
236
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
23
votes
0
answers
571
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
9
votes
1
answer
362
views
What are the differences and similarities between records, coinductive records, and codatatypes?
Record types are a common feature in most paradigms.
Agda also allows defining records with the coinductive keyword.
Lastly there are the seemingly more exotic co(...
- 319
8
votes
1
answer
159
views
Is it possible to define `fib` coinductive stream w/o sized types?
In Agda with --guardedness, we can define productive definitions using copatterns like the following
...
- 6,316