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 complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus 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 history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal-logic model model-category-theory monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories 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 stack string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topological 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.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 13th 2012

    Based on a private discussion with Mike Shulman, I have added some explanatory material to inductive type. This however should be checked. I have created an opening for someone to add a precise type-theoretic definition, or I may get to this myself if there are no takers soon.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2012
    • (edited Jan 13th 2012)

    I have taken the liberty to replace the four words “As a reality check” with the sentence: “Notice that these axioms still imply that algebra maps out of WW are essentially unique, even though that is not stated explicitly. ” Hope that’s okay.

    Also I have added some hyperlinks.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 13th 2012

    Thanks, this is great! I added a few more comments.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 13th 2012

    Actually, I liked the way I had it (“as a reality check”, etc.). Those particular words are not so important, but the point is to check that we get the usual notion of initial algebra on the nose in the case where equality is extensional. Yes, this might be considered trivial, but it’s good pedagogy for readers who have spent most of their lives thinking of equality as extensional, and IMO we should be very gentle in easing people into intensional type theory or homotopy type theory (as I can attest, being someone who has found this material very hard to follow).

    The comments Mike added to the page (thanks, Mike!) then lead naturally to the meaning of the words “essentially unique” (unique up to contractible space of choices).

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2012

    the point is to check that we get the usual notion of initial algebra on the nose in the case where equality is extensional.

    Yes, and this is what my sentence tries to say explicitly. When I first read your “as a reality check” I was confused about what it is you were going to check.

    If my sentence doesn’t cut it, replace it by another one. But I think it helps the reader to say in advance which reality it is that is going to be checked.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 13th 2012

    Urs #5: okay, I see what you’re saying. Does it read better now than it did?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2012
    • (edited Jan 13th 2012)

    I don’t find “As a reality check” to be a useful phrase. Why not say explicitly “Let’s check that indeed if … then …”?

    But if you don’t like it, I won’t object further.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 13th 2012

    Okay, I got rid of this phrase. I’ll suppose it now reads okay unless you tell me otherwise.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2012
    • (edited Jan 13th 2012)

    Yes, this I like! Thanks.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2012

    I have added to inductive type a link to a recent paper on the arXiv about homotopy-initiality of inductive types in homotopy type theory. See also a HoTT blog post.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 20th 2012

    Thank you, Mike! This looks very useful.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    I am working on prettifying and expanding inductive type (didn’t get very far yet, though).

    Here is one dumb little question on the most basic of all examples. I nevertheless have this question at the moment:

    when we write the endofunctor whose initial algebra is the natural numbers object as F(X)=1+XF(X) = 1+ X (instead of equivalently F(X)=*XF(X) = * \coprod X) it looks very nicely suggestive: by Lambek’s theorem the natural numbers are a fixed point of this functor, and so it seems suggestive to read F(X)=1+XF(X) = 1 + X as saying “The natural numbers are the universal thing that does not change when you add one component.”

    Nice. But then, when one looks at how an inital algebra for this FF gives a natural number object, it is not the “1”-summand above that induces the successor function. The 1-summand induces the 0-element

    (zero,successor):*XX. (zero, successor) : * \coprod X \to X \,.

    Sorry for this stupidity, but do you see what I am wondering about? On the one hand the “1+” in “1+X1+ X” seems related to the successor, in the other to the 0.

    How should I think about this, morally?

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    I have spelled out at inductive type in the section Examples - Natural numbers (scroll down to what currently is “Example 1”) a detailed walk through how the induction principle works for an \mathbb{N}-dependent proposition, in terms of the categorical semantics of elimination and computation rules.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    The “1+” is related to the 0, not the successor. If you want to say “The natural numbers are the universal thing that does not change when you add one component” then you can think about taking the whole natural numbers and shifting them up one in order to “add one component” at the bottom, namely 0. (I’m actually not sure how you could “add one component” to the “top” of the natural numbers and leave it unchanged…)

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 11th 2012

    Just Hilbert’s hotel, no?

    You can better get used to avoiding the +1 trap, by turning things about and thinking about coalgebras.

    X1+XX \to 1 + X,

    which is certainly not about adding anything. Part of XX gets killed, the rest are moved within XX.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2012

    Ah, I see. Thanks.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2012
    • (edited May 11th 2012)

    Coming back to the point discussed at the beginning of this thread here, that there are these two equivalent formulations of initial FF-algebra:

    1. WW is initial if there is a unique homomorphism to any other FF-algebra

    2. WW is initial if the slice over WW, as algebras, is pointed

    There is a deeper duality to this, right? The second is what is induction as such, whereas the first is recursion.

    Since it’s equivalent, it may seem strange to make the distinction. But it is true that the induction principle verbatim as traditionally stated comes out with the second definition.

    In Awodey-Gambino-Sojakova (but probably not just there) I see this distinction made around page 9. Also with different names for the type theory rules: simple elimination in the first case as opposed to the standard elimination in the second.

    I am just saying this to check if I am missing something. If not, I will work some remarks along these lines into the entry.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2012

    Yes, that’s right. And it’s important in type theory, for the reasons you mention. The “standard” elimination can also be called dependent elimination for clarity (since the type being eliminated into may depend on WW itself). The really nifty thing, I think, is that dependent elimination gives us a (homotopy) initial algebra, in particular a unique morphism into any other algebra, without our having to explicitly assert any uniqueness (and in particular without referring explicitly to any notion of “equality”).

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeMay 13th 2012

    It’s a mistake to say that 00 corresponds to 1+1 +. Rather, 00 corresponds to 11. The ++ is different. This may make it harder to mix things up. Otherwise I agree with Mike #14.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 18th 2012

    I have added to inductive type in the Examples section the missing subsection Path recursion to go with the section Path induction that was there before.

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)