2
$\begingroup$

Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and left on me an impression of something like a text by Conan Doyle abruptly interrupted at the most thrilling moment.

Could somebody update me on it? What happened afterwards? Most intriguing question that remains unanswered there is whether one can construct a more or less complete duality between inductive and coinductive types. The phenomenon of limit-colimit coincidence somehow suggests that in at least some circumstances that stem from endofunctors in the category-theoretic semantics, the types that correspond to initial algebras and final coalgebras of these endofunctors should be equivalent in some sense. There is a controversy in that discussion whether to expect that.

As an aside, let me remark that there does not even seem to exist any tags related to coinduction here.

| cite | improve this question | |
$\endgroup$
  • $\begingroup$ This happened. I can provide more references if needed. $\endgroup$ – Andrej Bauer Nov 20 at 14:46
  • $\begingroup$ @AndrejBauer Please do! More importantly, please say few more words about it. $\endgroup$ – მამუკა ჯიბლაძე Nov 20 at 16:05
  • 1
    $\begingroup$ One note about the paper mentioned by Andrej: The construction of final coalgebras from final coalgebras has been investigated as a form of completion, see Terminal coalgebras in well-founded set theory by Michael Barr, as the mentioned paper shows that this construction can be carried out in HoTT. The problem in plain MLTT, as you have seen in the mentioned discussion, is that equality usually does not play along with this construction. Instead, one needs to enforce bisimilarity somewhere. Also, please note that this does not mean initial algebras and final coalgebras coincide! $\endgroup$ – Henning Basold Nov 23 at 10:19
  • $\begingroup$ Unfortunately, this is not ripe for an answer. But I had a student who recently showed how coinductive types can get the right notion of equality in various ways. For instance, eta-equivalence + univalence, bisimilarity + coherence, or finality + coherence. This is similar to what the HoTT book does for inductive types. He then showed that these are all equivalent. What is interesting about this is that it shows that coinductive types need some extra assumption if you want to have that equality coincides with bisimilarity on coinductive types. I hope to find time for the paper soon! $\endgroup$ – Henning Basold Nov 23 at 10:24
  • $\begingroup$ One other tidbit is that cubical Agda has shown a very natural way for equality of coinductive types to work. Bisimulation can easily be given as/shown equivalent to a corecursive definition I -> T, which is the way paths are presented. So similar theories almost automatically make proper coinductive equality proofs just as natural as inductive equality proofs. $\endgroup$ – Dan Doel Nov 23 at 16:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.