Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeOct 4th 2012
   • (edited Oct 4th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 27th 2018
   • (edited Feb 27th 2018)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhere have people got to with coinductive types? I understand there was a technical obstacle, as [outlined](https://homotopytypetheory.org/2012/01/19/inductive-types-in-hott/#comment-1243) by Mike, and then a considerable [conversation](https://groups.google.com/forum/#!msg/homotopytypetheory/tYRTcI2Opyo/PIrI6t5me-oJ). I see people are still thinking about them, such as these posts by Egbert Rijke ([here](https://egbertrijke.com/2016/10/06/what-i-learned-this-summer-about-coinductive-types/) and [here](https://egbertrijke.com/2016/10/18/the-coinductive-type-generated-by-a-pointed-connected-type/)) Is [Non-well founded trees in Homotopy Type Theory](https://arxiv.org/abs/1504.02949) 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 27th 2018
   • (edited Feb 27th 2018)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIn 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](https://math.stackexchange.com/q/2113586/368788) *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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRight, 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI added a section at [[coinductive type]]. No doubt it could be improved. By the way, do you still agree with your earlier self [here](https://golem.ph.utexas.edu/category/2011/07/coinductive_definitions.html): >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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 27th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexProbably. I haven't thought about $\omega$-categories for a long time.

   Probably. I haven’t thought about $\omega$-categories for a long time.

7. • CommentRowNumber7.
   • CommentAuthorVictor Sannier
   • CommentTimeDec 15th 2023
   • (edited Dec 15th 2023)
   • PermaLink
   Author: Victor Sannier
   Format: MarkdownItexAdded examples of coinductive types I plan to create a page on [[conatural numbers]] in the near future. <a href="https://ncatlab.org/nlab/revision/diff/coinductive+type/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/coinductive+type/8">v8</a>, <a href="https://ncatlab.org/nlab/show/coinductive+type">current</a>

   Added examples of coinductive types

   I plan to create a page on conatural numbers in the near future.

   diff, v8, current

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 16th 2023
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWould need some unifying with example 1 at [[corecursion]], where they're called extended natural numbers.

   Would need some unifying with example 1 at corecursion, where they’re called extended natural numbers.

9. • CommentRowNumber9.
   • CommentAuthornLab edit announcer
   • CommentTimeJan 3rd 2024
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexUpdated reference information to: * {#ACS15} [[Benedikt Ahrens]], [[Paolo Capriotti]], [[Régis Spadotti]], *Non-wellfounded trees in Homotopy Type Theory*, in 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015) ([doi:10.4230/LIPIcs.TLCA.2015.17](https://doi.org/10.4230/LIPIcs.TLCA.2015.17), [arXiv:1504.02949](https://arxiv.org/abs/1504.02949)) Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/coinductive+type/9">diff</a>, <a href="https://ncatlab.org/nlab/revision/coinductive+type/9">v9</a>, <a href="https://ncatlab.org/nlab/show/coinductive+type">current</a>

   Updated reference information to:

   • {#ACS15} Benedikt Ahrens, Paolo Capriotti, Régis Spadotti, Non-wellfounded trees in Homotopy Type Theory, in 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015) (doi:10.4230/LIPIcs.TLCA.2015.17, arXiv:1504.02949)

   Anonymouse

   diff, v9, current