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 categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology 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 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 limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology natural 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 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.
    • 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.

    • CommentRowNumber21.
    • CommentAuthorGuest
    • CommentTimeAug 25th 2020
    Can anybody explain why the initial X with commutative triangle A -> X -> A x A = A -> AxA isn’t just X =A?
    • CommentRowNumber22.
    • CommentAuthorGuest
    • CommentTimeAug 25th 2020
    Perhaps it’s because the map A -> AxA is not a fibration, just an ordinary morphism, and X with it’s triangle structure is initial among fibrations
    • CommentRowNumber23.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 25th 2020
    • (edited Aug 25th 2020)

    Nice question! The entry is very confusing, and I think wrong. The reason that Δ:AA×A\Delta: A \rightarrow A \times A is not initial would be that it does not necessarily have the required uniqueness property. But I don’t think that it makes any sense to say that the path object is initial either. The path object is not even precisely defined currently: the properties listed at path space object are somewhat vague. One thing we can note that is that if we have a retraction pp of the arrow c:AA Ic: A \rightarrow A^I available, such that cpc \circ p is homotopic to the identity, then this retraction allows us to construct an algebra morphism from A IA×AA^I \rightarrow A \times A to any EA×AE \rightarrow A \times A up to homotopy. But I don’t see any reason to be able to even construct such a morphism on the nose, never mind the uniqueness property. We can also note that this is not a matter of extensional vs intensional type theory: the best one can hope for is that cpc \circ p is isomorphic to the identity, it will never be equal to the identity.

  1. It might be true that, when everything is precisely formulated, one can demonstrate homotopy initiality in some sense. But a) I’d like to see that written down carefully, and b) in that case, since we will have that Δ:AA×A\Delta: A \rightarrow A \times A is homotopy equivalent as an algeba to the path fibration, we would actually be able to take Δ:AA×A\Delta: A \rightarrow A \times A to be initial, and use of the path fibration is somewhat redundant.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeAug 25th 2020

    Yeah, the page inductive type is wrong as stated. If we refer to an initial object in a 1-category, then we get the diagonal. If we refer to an initial object in an (,1)(\infty,1)-category, then we get anything equivalent to the diagonal, which includes the path space object but also the diagonal itself. The only way we specifically get the path space object is if we require the inductive type to be a fibration, but in that case it’s not strictly initial any more.

    Probably the right thing to do is rework the whole entry to be more precise, and distinguish between syntactic inductive types and their various semantic incarnations.

    • CommentRowNumber26.
    • CommentAuthorDean
    • CommentTimeAug 26th 2020

    Nonetheless, the identity type works on a similar setup. I think it’s because we have to require the map X -> A xA to be a fibration in the universal property. A -> A xA is not a fibration, but the universal fix is the path space map A^I -> AxA. There the fibers are Id_A(x, y). I’m actually not sure about this, but my hunch is based on which maps are fibrations in the identity type. Your thoughts?

    • CommentRowNumber27.
    • CommentAuthorDean
    • CommentTimeAug 26th 2020

    So (just to be clear) the hunch I have at a fix is that

    1) we consider commutative triangles A -> X -> A xA = A -> AxA where X -> AxA is a fibration.

    2) a morphism of such diagrams A -> X -> A xA = A -> AxA and A -> Y > A xA = A -> AxA is a fibration X -> Y such that the resulting diagrams commute.

    3) A -> A^I -> AxA is initial among such diagrams.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2020
    • (edited Aug 26th 2020)

    The entry is clearly stubby: its very first line is requesting – since rev 10 from 8 years ago – the syntactic definition to be filled in.

    That said, the statement you seem to be discussing is in a section explicitly titled “Semantics” and there moreover after restricting attention to 1-categories.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2020

    @Dean: Yes, that’s what I was talking about with ” The only way we specifically get the path space object is if we require the inductive type to be a fibration, but in that case it’s not strictly initial any more.”

    • CommentRowNumber30.
    • CommentAuthorGuest
    • CommentTimeAug 27th 2020
    Oh, I see now.
    • CommentRowNumber31.
    • CommentAuthorDean
    • CommentTimeAug 28th 2020
    By the way, @Mike, I was wondering what would happen if we have loop space objects and suspension objects in a type theory and require these to be inverse. Do we get spectra?

    Probably you know the answer to this.
    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeAug 28th 2020

    Dean, this is discussed in section 2.2 of Schwede 97.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeAug 28th 2020
    • (edited Aug 28th 2020)

    To get spectra, one needs to invert not only ΣΩ\Sigma \Omega itself, but also its action “on finite pointed powers”, in the sense of Prop. 4.7 here.

    (This is an abservation due to Goodwillie, follow the pointers behind the above link.)

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeAug 28th 2020

    I think you may be thinking of a different sense of “invert”, Urs. It is true that a pointed (,1)(\infty,1)-category in which the adjunction ΣΩ\Sigma \dashv \Omega is an equivalence is necessarily stable. This is not really “type theory” though, at least not in the sense of HoTT, since pointed and stable (,1)(\infty,1)-categories do not model HoTT. Although there is now a variant of HoTT that is expected to have models in parametrized spectra and in which ΣΩ\Sigma\dashv\Omega is an equivalence for the “stable” objects (the spectra over a point).

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2020

    Check out the pointer I gave, Prop. 4.7 here, this is about localization in infinity-toposes yielding parametrized spectra.

    And it’s exactly what Anel-Finster-Joyal considered.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeAug 29th 2020

    Right. As I said, that is a different sense of “invert”. Dean’s question asked about Σ\Sigma and Ω\Omega being inverses, not about objects that see them as inverses.

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2020

    That hair can hardly be split: Once localized. it is what the objects think it is, that’s Yoneda.

    If you or Dean feel like providing the precise detail that you would actually like to see discussed, that might make for a more fruitful conversation.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeAug 30th 2020

    The hair is split by (1) well-typedness, since one question is about a property of a category and the other is about an operation on a category or a subclass of objects, and (2) the fact that the answers are different. I don’t think anyone is saying something should be added to the lab, Dean was just asking a question.

    • CommentRowNumber39.
    • CommentAuthorDean
    • CommentTimeSep 3rd 2020

    @Mike Shulman: in 29, you’re saying it wouldn’t be inititial with fibrations as maps? Does this mean that the identity type is not unique up to isomorphism, or does it mean we’re missing some property of identity type? Sorry for having to clarify – I’m new to type theory.

    By the way, in type theory, I like as a semantics a strict 2-category, which makes things less confusing to me when we have to be rigorous about which things are fibrations in the semantics:

    We start with a strict 2-category UU with objects ** and Type\text{Type}. C:TypeC : \text{Type} is semantically a map *Type* \rightarrow \text{Type}. Context extension is a contravariant functor [*,Type]U[*, \text{Type} ] \rightarrow U. We also designate an object \star in [*,Type][*, \text{Type}], which we think of as terminal. It sends objects *Type* \rightarrow \text{Type} in [*,Type][*, \text{Type}] (which are 11-cells in UU) to objects in UU. I notate it by X[,Type]X \mapsto [-, \text{Type}], (f:XY)f *:[Y,Type][X,Type](f : X \implies Y) \mapsto f_* : [Y, \text{Type}] \rightarrow [X, \text{Type}]. Dependent sum and dependent product are the same except covariant, and notated f *f^* and f !f^!. We also must construct binary pullback and internal hom in each of these categories, and require f !f *Y=X×Yf^! f_* Y = X \times Y for f:X*f : X \implies *, and analogously for internal hom.

    To recover the 11-categorical semantics, let U=CatU = \text{Cat}, Let Type\text{Type} be a certain category CC, [X,C][X, C] is C/XC/X, f *f_* is pullback, etc.

    In homotopy type theory, UU is (,1)Cat(\infty, 1)-\text{Cat}, Type\text{Type} is the category of infinity groupoids, [X,C][X, C] is a functor, viewing the infinity groupoid XX as an (,1)(\infty, 1)-category, f *f_* is [f,C][f, C], etc.

    I think it’s easier to express the path space object in this semantics, since it is clearer how it comes from the identity type.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2020

    Yes, in MLTT and Book HoTT the identity type is not unique up to isomorphism. (In cubical type theory, which internalizes an interval object, there is an identity type satisfying a different “path space” universal property that does determine it up to isomorphism.) Note though that this semantic notion of “isomorphism” is not expressible internally (except in a two-level type theory), and the identity type is unique up to the strongest internally-expressible notion of equivalence.

    • CommentRowNumber41.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 4th 2021

    Is it standard, as on this page, to have induction as dependent elimination and recursion as elimination?

    Kevin Buzzard is talking about Lean here and seems to split it as recursion is dependent elimination over types, and induction as dependent elimination over propositions.

    Isn’t that the more familiar split of recursion as arrow out of initial object and induction as only identity as sub-algebra of initial algebra?

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)