Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I got annoyed that so many pages were asking to link to coinductive type without that page being existent. So I started something. For the moment it is essentially just a glorified redirect.
Where have people got to with coinductive types? I understand there was a technical obstacle, as outlined by Mike, and then a considerable conversation.
I see people are still thinking about them, such as these posts by Egbert Rijke (here and here)
Is Non-well founded trees in Homotopy Type Theory about as far as people have got, and perhaps as far as one can go, given the this asymmetry:
The universal property defining (internal) coinductive types in HoTT is dual to the one defining (internal) inductive types. One might hence assume that their existence is equivalent to a set of type-theoretic rules dual (in a suitable sense) to those given for external W-types as in item 2 above. However, the rules for external W-types cannot be dualized in a naïve way, due to some asymmetry of HoTT related to dependent types as maps into a “type of types” (a universe), see the discussion in [9]. In this work, we show instead that coinductive types in the form of M-types can be derived from certain inductive types.
In that Homotopy Type Theory Google group, Mike said
to formulate a “coinduction principle” generally that’s dual to an induction principle, one seems to need some kind of “codependent types”.
But in answer to a Math stack exchange question Is there a notion of “codependent” types for coinductive types?, this reply isn’t challenged:
There is a dual notion of coinductive types, yes, and we don’t need to look past the framework of dependent types.
Right, it depends on how you want to say “coinductive type”. If you want to dualize completely the usual rules for inductive types, including dualizing the induction principle to a “coinduction principle”, then you do seem to need “codependent types”. (We might actually be inching closer to “codependent types”, with the introduction of rules for “cofibrations” such as in Riehl-Shulman, but I think we’re still a ways from understanding them well enough to formulate a coinduction principle.) But you can instead dualize the alternative characterization of inductive types as initial algebras to get a notion of coinductive types as terminal coalgebras, and that can be formulated (and often constructed) in ordinary HoTT.
I added a section at coinductive type. No doubt it could be improved.
By the way, do you still agree with your earlier self here:
I’ve come to believe, over the past couple of years, that anyone trying to study $\omega$-categories (a.k.a. $(\infty,\infty)$-categories) without knowing about coinductive definitions is going to be struggling against nature due to not having the proper tools.
Probably. I haven’t thought about $\omega$-categories for a long time.
Added examples of coinductive types
I plan to create a page on conatural numbers in the near future.
Would need some unifying with example 1 at corecursion, where they’re called extended natural numbers.
Updated reference information to:
Anonymouse
1 to 9 of 9