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

Discussion Tag Cloud

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

nLab > Latest Changes: dependent product

Bottom of Page

1 to 23 of 23

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2011
    • (edited Oct 2nd 2012)

    I did the following to dependent product:

    • rearranged the section outline somewhat

    • added the statement that in type theory ∏ x∈XP x\prod_{x \in X} P_x may be written ∀x:X,Px\forall x : X , P x;

    • added a Properties-section

    • added statement and proof of the relation of dependent product to spaces of sections

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2011

    added a pointer to this discussion also to the homotopy type theory / homotopy theory - dictionary

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeNov 4th 2011
    • (edited Nov 4th 2011)

    I don’t really like your remarks about type theory. Not all type theory uses the same notation for propositions as for types, and they (usually) use ‘dependent product’ in the same way that we do. (Somebody added a remark that some type theorists use the term in a funny way, and that may be so, but I’ve never seen it; in any case, it’s wrong to claim this of type theorists in general.

    Also, this is our only article on dependent sums (which are a simpler concept), so they shouldn’t be stuck in the Properties. So I rearranged things a bit some more.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2011

    I don’t really like your remarks about type theory.

    Which remarks do you mean?

    Also, this is our only article on dependent sums (which are a simpler concept), so they shouldn’t be stuck in the Properties.

    They should eventually have their own entry. I’d argue that before my last edit the situation was even worse. But eventually we’ll produce a nice entry here.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2011

    I changed “often” to “sometimes (as in Coq)”. I’ve actually seen that notation for dependent products quite rarely aside from in Coq code.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeNov 4th 2011

    I don’t really like your remarks about type theory.

    Which remarks do you mean?

    Only the ones that I changed.

    I’d argue that before my last edit the situation was even worse.

    I’m not disputing that!

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2011
    • (edited Nov 4th 2011)

    Which remarks do you mean?

    Only the ones that I changed.

    Please be less cryptic! I don’t think I made any remark about type theory. So please tell me explicitly what it is you are disagreeing with. Because: otherwise you confuse me! :-)

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011

    OK, let’s see … You wrote that dependent products are written like universal quantification in type theory, whereas this is only done when doing propositions as types (and not even always then, since one can always write things the other way instead). You wrote that the dependent product is called ‘dependent sum’ in that context (type theory, tout court), whereas I have never seen this and the original comment was only that this happens sometimes.

    So basically, what I mentioned in my original comment.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2011

    You wrote that dependent products are written like universal quantification in type theory, whereas this is only done when doing propositions as types (and not even always then, since one can always write things the other way instead).

    Okay, so I have added the qualifier “if one considers propositions as types” to the entry.

    You wrote that the dependent product is called ‘dependent sum’ in that context

    No, I didn’t write that. Somebody else did. It just looks as if I wrote this in the history because I gave it a different subsection or something, and the software sometimes can’t distinguish between new text and text that was moved a little.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011

    Okay, so I have added the qualifier “if one considers propositions as types” to the entry.

    I already did that, where it was needed for precision. I don’t think that it’s necessary in the analogy where you put it now.

    No, I didn’t write that.

    What had been there before was different. You changed it, probably inadvertently.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2011
    • (edited Nov 7th 2011)

    You wrote that the dependent product is called ‘dependent sum’ in that context

    What I wrote, back in September 2010, is that the dependent sum is sometimes called the dependent product, not the other way ’round. That’s the one that at least makes a little sense, since dependent sum generalizes binary product. Analogously to that terminology, one might call (what we call) the dependent product a “dependent function space” (and some people do).

    I added this back into the page, since I think it is a useful warning.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011
    • (edited Nov 7th 2011)

    Urs never had this backward; I did (and only in comment #8, not in the page or even in comment #3). And I don’t think that I meant to remove that warning entirely, but apparently I did, oops!

    A dependent sum is a kind of product in the Calculus of Constructions (Coq) library of head-normal forms. But it seems wrong to me to call it a dependent product. Do you recall who does that?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 8th 2011

    I agree that it’s wrong. I don’t remember where I heard it, sorry; it might have just been some type theorist telling me that some other type theorists do it.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012

    I created dependent sum type (by copying stuff from product type) and dependent product type (copying from function type).

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012

    I have tried to brush-up dependent product a little.

    • gave the Idea-section two new sentences right at the beginning in an attempt to say right away what the entry is about;

    • tried to disentangle the various things said in the Definition-section, in part by moving stuff to the Properties-section.

    More could be done here. But I need to quit for the moment.

    • CommentRowNumber16.
    • CommentAuthorNikolajK
    • CommentTimeMar 18th 2015
    • (edited Mar 18th 2015)

    In base change, and maybe somewhere else, the ∏ f\prod_f and ∑ f\sum_f notation is in use, parallel with the f *f_* and f !f_! notation. It’s not clear to me if or how they really differ.

    Moreover, in dependent product we have two functors from g:B→Ag:B\to A, the ∏ g\prod_g which maps between two slice categories bfC/B→bfC/A{\bf{C}}/B\to{\bf{C}}/A, and then the product which maps from a slice category bfC/X{\bf{C}}/X to the category bfC{\bf{C}} itself. It’s not explicitly said what the mappings at work really are. The functor in the other direction is denoted −×X- \times X and the product seems to be defined as adjoint to it. Is the mapping from objects TT to projections p T:(T×X)→Xp_T:(T \times X)\to X? We have a link to the object/space of sections page, but this one refers back to the product. What also “bothers me” is that it seems I can’t use this to define the exponential object as special case of it, because the requirement stated says we a priori look at a CCC.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMar 18th 2015
    • (edited Mar 18th 2015)

    Regarding the second (or so) aspect: the functor (−)×X(-)\times X is the special case of pullback base change along morphisms of the form X→*X \to \ast (to the terminal object). And notice that 𝒞≃𝒞 /*\mathcal{C}\simeq \mathcal{C}_{/\ast}.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMar 18th 2015

    There is no difference between Σ f/Π f\Sigma_f/\Pi_f and f !/f *f_!/f_*. The exponential object Y XY^X is obtained as the composite of pullback along X→*X\to \ast followed by the dependent product along that map. Where are you seeing the requirement of being a priori in a CCC?

    • CommentRowNumber19.
    • CommentAuthorNikolajK
    • CommentTimeMar 19th 2015
    • (edited Mar 19th 2015)

    Thanks both. Under the proposition giving the special case of the exponential object, I’ve now written the example of C=SetC=Set, making the construction explicit for sets and functions.

    • CommentRowNumber20.
    • CommentAuthorRodMcGuire
    • CommentTimeMar 19th 2015
    • (edited Nov 24th 2019)

    I just noticed that dependent+product+natural+deduction+-+table displays broken images.

    I made a new nForum thread to discuss this issue: Quicklatex dead cache problems

    EDIT: changed link from mathforge to ncatlab

  21. “It generalizes the internal hom, and hence indexed products”

    I don’t see how the internal hom generalizes indexed products. Hom(A,B)\text{Hom}(A, B) is weaker than a product of subobjects of BB indexed by elements of AA, since it forgets to which subobject each index is mapped to.

    I would say that: - The internal hom internalizes the hom set, the set Hom(A,B)\text{Hom}(A, B) of morphisms A→BA \to B; the object [A,B][A, B] mimics this set - The dependent product internalizes indexed products, the set Π a∈AB a\Pi_{a \in A} B_a of morphisms A→B=⋃ a∈AB aA \to B = \bigcup_{a \in A} B_a where each a∈Aa \in A is mapped to some b∈B ab \in B_a - The indexed product generalizes the hom set (the hom set is the indexed product with B a=BB_a = B) - Similarly, the dependent product generalizes the internal hom, not the other way around.

    Stefan

    diff, v52, current

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeNov 24th 2019

    I think I agree, I’m not sure what that “hence” was intended to mean.

    • CommentRowNumber23.
    • CommentAuthorziggurism
    • CommentTimeFeb 25th 2020

    exponential object is a “constant” dependent product is a categorified version of the fact that exponentiation of numbers is repeated multiplication. not of the fact that multiplication is repeated addition

    diff, v53, current

1 to 23 of 23

  1.