Questions tagged [coinductive-type]

Use with coinductive types.

Filter by
Sorted by
Tagged with
22 votes
1 answer

What is the state of coinductive types and reasoning in Coq?

Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
palmskog's user avatar
  • 395
12 votes
1 answer

Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as Inductive ord := O | S (n: ord) | Lim (s: nat -> ord). Suppose you use the following encoding instead ...
Molly Stewart-Gallus's user avatar
18 votes
1 answer

When to use coinductive types?

One could define streams in the following manner ...
Agnishom Chattopadhyay's user avatar
2 votes
1 answer

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

Suppose we work inside MLTT with equality reflection (extensional MLTT). Assume I postulate existence of Streams as final co-algebra for the suitable functor. Is that enough to prove the bisimulation ...
Russoul's user avatar
  • 345