Not signed in (Sign In)

Start a new discussion

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 galois-theory 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 manifolds 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 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 simplicial space spin-geometry stable-homotopy-theory string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 8th 2010

    Created W-type.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 8th 2010

    And a related query at pretopos.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 22nd 2012

    Added to W-type a section Properties with a pointer to Danielsson’s recent post.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2014

    added to W-type pointers to

    • the article by Gambino-Hyland on dependent W-types

    • the article by van den Berg and Moerdijk on W-types in model categories (those given by fibrations)

    Also made the following trivial edit: changed the name of the ambient category from CC to 𝒞\mathcal{C} as it seemed rather bad style to have a category named CC with objects named AA, BB and DD.

    I’ll have a question or comment on W-types in linear type theory, but I’ll put that in a separate thread…

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2014
    • (edited Jan 18th 2014)

    Heh, you changed the name from a recognizable letter to a nondescript grey box, according to my Firefox for Android. But that’s OK, I don't think that we should actually cater to that.

  1. Reference to Michael Abbott, Thorsten Altenkirch, and Neil Ghani, Representing Nested Inductive Types using W-types


    diff, v29, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 25th 2019
    • (edited Jul 25th 2019)

    Thanks for editing.

    Allow me to mention some hints on formatting references:

    • leave a whitespace to any previous text, not to have the output clutter

    • a * followed by a whitespace right at the beginning of the line makes a bullet item for the reference to fit into the rest of the list

    • enclosing author names in double square brackets hyperlinks them to their pages

    • explicit hyperlinks need the http://-prefix to be parsed

    I have slightly reformatted accordingly, now the source looks like so

      * [[Michael Abbott]], [[Thorsten Altenkirch]], and [[Neil Ghani]], 
      _Representing Nested Inductive Types using W-types_ 

    and renders like so:

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeJul 25th 2019
    Re #6. Thanks! I'll try to remember that.
    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 1st 2021

    Added reference

    diff, v32, current

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 13th 2021

    Spencer Breiner pointed out on Zulip that this page claims that natural numbers (and lists) are W-types, when type-theoretically they are actually not. In type theory, a W-type has only one constructor, while nat and lists have two constructors. They can be encoded as W-types using a sum-type to wrap up the two constructors into one, but the result doesn’t have the same computation rules and requires function extensionality for its correctness. So I removed these examples from this page and put the corresponding text at inductive type.

    diff, v33, current

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 13th 2021
    • (edited Aug 13th 2021)

    A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”. It is thus a particular kind of inductive type, with one constructor having a certain canonical form.

    How’s that “thus” working? Why “one constructor” in this concept.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2021

    Maybe we should just omit “thus”. Would it make sense that way?

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 14th 2021

    Have written it as

    A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”, with one constructor having a certain canonical form. As such it is a particular kind of inductive type.

    The page still contains a query from you Mike:

    Is the term “W-type” still used in this generality? Or are they just called “inductive types”?

    Is this resolved yet?

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2021

    Clarified the situation with indices, parameters, and non-uniform parameters.

    diff, v35, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2021

    Thanks for pointing that out, have now resolved it.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)