Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I did the following to dependent product:
rearranged the section outline somewhat
added the statement that in type theory $\prod_{x \in X} P_x$ may be written $\forall x : X , P x$;
added a Properties-section
added statement and proof of the relation of dependent product to spaces of sections
added a pointer to this discussion also to the homotopy type theory / homotopy theory - dictionary
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.
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.
I changed “often” to “sometimes (as in Coq)”. I’ve actually seen that notation for dependent products quite rarely aside from in Coq code.
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!
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! :-)
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.
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.
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.
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.
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?
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.
I created dependent sum type (by copying stuff from product type) and dependent product type (copying from function type).
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.
In base change, and maybe somewhere else, the $\prod_f$ and $\sum_f$ notation is in use, parallel with the $f_*$ and $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\to A$, the $\prod_g$ which maps between two slice categories ${\bf{C}}/B\to{\bf{C}}/A$, and then the product which maps from a slice category ${\bf{C}}/X$ to the category ${\bf{C}}$ itself. It’s not explicitly said what the mappings at work really are. The functor in the other direction is denoted $- \times X$ and the product seems to be defined as adjoint to it. Is the mapping from objects $T$ to projections $p_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.
Regarding the second (or so) aspect: the functor $(-)\times X$ is the special case of pullback base change along morphisms of the form $X \to \ast$ (to the terminal object). And notice that $\mathcal{C}\simeq \mathcal{C}_{/\ast}$.
There is no difference between $\Sigma_f/\Pi_f$ and $f_!/f_*$. The exponential object $Y^X$ is obtained as the composite of pullback along $X\to \ast$ followed by the dependent product along that map. Where are you seeing the requirement of being a priori in a CCC?
Thanks both. Under the proposition giving the special case of the exponential object, I’ve now written the example of $C=Set$, making the construction explicit for sets and functions.
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
1 to 20 of 20