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 beauty book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory 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 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 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.
    • 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

    Anonymous

    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_ 
      ([pdf](http://www.cs.nott.ac.uk/~psztxa/publ/icalp04.pdf))
    

    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.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 31st 2022
    • (edited Dec 31st 2022)

    I have added publication data to:

    I am guessing that this is the reference which was meant to be referred to at the end of this paragraph (where it had a broken anchor to [AAG](#AAG)) and so I fixed the link accordingly

    diff, v36, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023
    • (edited Jan 1st 2023)

    did a fair bit of rewording and adjustment in the Idea-section (here) for better (logical) flow

    switched to calligraphic “𝒲\mathcal{W}-type”, throughout

    switched the ordering of the subsections “In category theory”, “In type theory”.

    The 𝒲\mathcal{W}-type inference rules here had a query box comment:

    Andreas Abel: A and B are used exactly the other way round in the introductory text to this page. (Before, A was the arity, now B is the arity.) Harmonize!?

    Indeed. Am harmonizing this now by using, throughout:

    • CC” for the type of constructors

    • AA” for the type of arities.

    introduced formatting of 𝒲\mathcal{W}-type denotation as “𝒲c:CA(c)\underset{c \colon C}{\mathcal{W}} \, A(c)

    diff, v37, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023

    fixed these bibitems:

    diff, v37, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023

    adjusted the typesetting of the type inference rules, in particular:

    • added more widespace to make it easier on the eye to recognize the syntax tree branching

    • chose more suggestive term names

    now it looks as follows:


    (1) type formation rule:

    C:Type;c:CA(c):Type| || |𝒲c:CA(c):Type \frac { C \,\colon\, Type \;; \;\;\; c \,\colon\, C \;\;\vdash\;\; A(c) \,\colon\,Type \mathclap{\phantom{\vert_{\vert}}} } { \mathclap{\phantom{\vert^{\vert}}} \underset{c \colon C}{\mathcal{W}}\, A(c) \,\colon\, Type }

    (2) term introduction rule:

    root:C;subtr:A(c)𝒲c:CA(c)| |tree(root,subtr):𝒲c:CA(c) \frac{ \vdash\; root \,\colon\, C \;; \;\; subtr \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) }{ \mathclap{\phantom{\vert^{\vert}}} tree\big(root ,\, subtr\big) \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) }

    (3) term elimination rule:

    t:𝒲c:CA(c)D(t):Type; root:C,subt:A(c)𝒲c:CA(c),subt D:a:A(root)D(subt(a)) tree D(root,subt,subt D):D(tree(c,subt))| || |t:𝒲c:CA(c)wrec (D,tree D)(t):D(t) \frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,, \; subt \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a \colon A(root)}{\prod} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt ,\, subt_D\big) \,\colon\, D\big(tree(c,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \mathclap{\phantom{\vert^{\vert}}} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; wrec_{(D,tree_D)}(t) \,\colon\, D(t) }

    (4) computation rule:

    t:𝒲c:CA(c)D(t):Type; root:C,subt:A(c)𝒲c:CA(c),subt D:Πa:A(c)D(subt(a)) tree D(root,subt,subt D):D(tree(root,subt))| || |root:C,subtr:A(c)𝒲c:CA(c) wrec (D,tree D)(tree(root,subtr))=tree D(root,subt,λa.wrec (D,tree D)(subtr(a))) \frac{ \begin{array}{l} t \,\colon\, \underset{c \colon C}{\mathcal{W}}\, A(c) \;\vdash\; D(t) \,\colon\, Type \;; \\ root \,\colon\, C \,,\; subt \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \,, \; subt_D \,\colon\, \underset{a\colon A(c)}{\Pi} D\big(subt(a)\big) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; tree_D\big(root,\,subt,\,subt_D\big) \,\colon\, D\big(tree(root,\, subt)\big) \mathclap{\phantom{\vert_{\vert}}} \end{array} }{ \begin{array}{l} \mathclap{\phantom{\vert^{\vert}}} root \,\colon\, C \,, \;\; subtr \,\colon\, A(c) \to \underset{c \colon C}{\mathcal{W}}\, A(c) \\ \;\;\;\;\;\;\;\;\;\;\; \;\;\vdash\;\; wrec_{(D,tree_D)}\big( tree(root, \, subtr) \big) \;=\; tree_D \Big( root ,\, subt ,\, \lambda a . wrec_{(D,tree_D)}\big(subtr(a)\big) \Big) \end{array} }

    diff, v37, current

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023
    • (edited Jan 1st 2023)

    added pointer to:

    diff, v38, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2023

    made explicit the example of the natural numbers W-type with a numbered environment (here)

    diff, v38, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2023

    organized all references on semantics of W-types by initial endofunctor algebras: here

    (cf. nForum announcement here)

    diff, v40, current

    • CommentRowNumber23.
    • CommentAuthorncfavier
    • CommentTimeMar 3rd 2023
    • (edited Mar 3rd 2023)

    mentioned that the dependent product is not dependent in the plain case by factoring through the reader monad

    diff, v42, current

    • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 3rd 2023

    In the sentence

    More generally, endofunctors that look like polynomials in the traditional sense:

    F(Y)=A n×Y ×n++A 1×Y+A 0 F(Y) = A_n \times Y^{\times n} + \dots + A_1 \times Y + A_0

    can be constructed as polynomial endofunctors in the above sense in any Π\Pi-pretopos.

    I changed the Π\Pi-pretopos to just a pretopos, since that is all one needs for the finite products and coproducts.

    diff, v43, current

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 6th 2023

    I plan to add in the morphism that makes the endofunctor in the previous comment polynomial, having now double checked it really works for an arbitrary pretopos. For a σ\sigma-pretopos (ie countable coproducts and corresponding extensivity) one gets analytic endofunctors (those that are formal power series) being polynomial for free as well. Then I’ll check about existence of W-types for these based just on having a parameterised NNO.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2023

    added earlier reference for the introduction of the notion of W-types:

    following a hint in another thread (here)

    diff, v47, current