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-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck 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 infinity integration integration-theory k-theory lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology newpage noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory 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

    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.
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)