Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 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 nforum nlab noncommutative noncommutative-geometry number-theory 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 sheaves 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012
    • (edited Oct 4th 2012)

    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.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 27th 2018
    • (edited Feb 27th 2018)

    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.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 27th 2018
    • (edited Feb 27th 2018)

    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.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 27th 2018

    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.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 27th 2018

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 27th 2018

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

    • CommentRowNumber7.
    • CommentAuthorVictor Sannier
    • CommentTimeDec 15th 2023
    • (edited Dec 15th 2023)

    Added examples of coinductive types

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

    diff, v8, current

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 16th 2023

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

  1. Updated reference information to:


    diff, v9, current