Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 28th 2012
   • (edited Sep 28th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI started creating the following tables for the entry _[[geometry of physics]]_. After having created them there I found that these deserve to be put into the related entries, too. So therefore I put them into their own pages now and included them in related entries via [[!include .... - table]] These are the tables that I have so far: * [[judgements for types and terms - table]] * [[product natural deduction - table]] * [[dependent sum natural deduction - table]] These need a bit mor attention. But I have to quit now for the time being. Also, I am afraid I may be running here again against Mike's preference for notation here and there. But I am not dogmatic about this, I just created these tables as they happened to occur to me. I try to polish them later.

   I started creating the following tables for the entry geometry of physics. After having created them there I found that these deserve to be put into the related entries, too. So therefore I put them into their own pages now and included them in related entries via

     [[!include .... - table]]
   

   These are the tables that I have so far:

   • judgements for types and terms - table

   • product natural deduction - table

   • dependent sum natural deduction - table

   These need a bit mor attention. But I have to quit now for the time being. Also, I am afraid I may be running here again against Mike’s preference for notation here and there.

   But I am not dogmatic about this, I just created these tables as they happened to occur to me. I try to polish them later.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexNo, I think I'm fine. (I'm sorry that I come across as so inflexible; I should probably relax some.) I removed some extra right parentheses in the product table, and added what seemed to me to be a missing $p_1$ in the dependent sum table --- although to be honest, I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn't really distinguish very well between the terms $a$ and $(a,b)$. Strangely, in my browser the equation $p_2(a,b)=b$ in the last row of the product table runs out of its cell and into the next one. I wonder why that could be?

   No, I think I’m fine. (I’m sorry that I come across as so inflexible; I should probably relax some.) I removed some extra right parentheses in the product table, and added what seemed to me to be a missing $p_1$ in the dependent sum table — although to be honest, I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn’t really distinguish very well between the terms $a$ and $(a,b)$.

   Strangely, in my browser the equation $p_2(a,b)=b$ in the last row of the product table runs out of its cell and into the next one. I wonder why that could be?

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2012
   • (edited Sep 29th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn’t really distinguish very well between the terms a and (a,b). Yes. I had the same thought. So I had first created the table for the products, of course, and then naively started doing the one for dependent sum "along the same lines" only to notice while doing so that it doesn't quite come out as nicely. The problem is of course that while its a "universal construction" of sorts, it's not quite (co)-limiting diagram over a simple finite diagram. But maybe it's still useful, anyway, for the reader to see the morphisms labled as far as it goes. > Strangely, in my browser the equation p 2(a,b)=b in the last row of the product table runs out of its cell and into the next one. Interesting. Same for me. I'll try to add some whitespace, like $\,$ sometimes that helps.

   I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn’t really distinguish very well between the terms a and (a,b).

   Yes. I had the same thought. So I had first created the table for the products, of course, and then naively started doing the one for dependent sum “along the same lines” only to notice while doing so that it doesn’t quite come out as nicely. The problem is of course that while its a “universal construction” of sorts, it’s not quite (co)-limiting diagram over a simple finite diagram. But maybe it’s still useful, anyway, for the reader to see the morphisms labled as far as it goes.

   Strangely, in my browser the equation p 2(a,b)=b in the last row of the product table runs out of its cell and into the next one.

   Interesting. Same for me. I’ll try to add some whitespace, like

     $\,$
   

   sometimes that helps.

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeOct 1st 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI don't think that the missing $p_1$ is supposed to be there, just as the corresponding $p_1$ and $p_2$ aren\'t in the product table. I mean, if I understand what these diagrams are supposed to be.

   I don’t think that the missing $p_1$ is supposed to be there, just as the corresponding $p_1$ and $p_2$ aren't in the product table. I mean, if I understand what these diagrams are supposed to be.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeOct 1st 2012
   • (edited Oct 1st 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> I don’t think Ah, that's right. Now I have looked at it. I had tried to mimic in the diagrams what happens in term introduction/elimination/computation by drawing only those arrows that interpret the given step. So * for term introduction only the arrows into the new object; * for term elimination those out of the object; * for computation both of them, hence the commuting diagram they form. But, as we said, for dependent sum this doesn't work quite as well as for products.

   I don’t think

   Ah, that’s right. Now I have looked at it.

   I had tried to mimic in the diagrams what happens in term introduction/elimination/computation by drawing only those arrows that interpret the given step. So

   • for term introduction only the arrows into the new object;

   • for term elimination those out of the object;

   • for computation both of them, hence the commuting diagram they form.

   But, as we said, for dependent sum this doesn’t work quite as well as for products.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeOct 1st 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>for computation both of them, hence the commuting diagram they form In fact, I would say: for computation, the commuting diagram (a 2-cell) they form, hence (necessarily as forming the boundary of that diagram) both of them.

   for computation both of them, hence the commuting diagram they form

   In fact, I would say: for computation, the commuting diagram (a 2-cell) they form, hence (necessarily as forming the boundary of that diagram) both of them.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeOct 1st 2012
   • (edited Oct 1st 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, good point. Maybe we should indicate the 2-cell. But that will blow up the size of the diagram a good bit... ... unless of course somebody feels inspired to create some SVG...

   Yes, good point. Maybe we should indicate the 2-cell. But that will blow up the size of the diagram a good bit…

   … unless of course somebody feels inspired to create some SVG…

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeOct 1st 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe $2$-cells are implicit in any diagram called commutative. Perhaps some explicit label is called for, but maybe we can leave it implicit.

   The $2$-cells are implicit in any diagram called commutative. Perhaps some explicit label is called for, but maybe we can leave it implicit.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeOct 1st 2012
   • (edited Oct 1st 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> The 2-cells are implicit in any diagram called commutative. Yeah, that's why I did the diagrams the way I did them. But I thought _you_ had just been suggesting in #6 to make them explicit. But never mind, I guess we agree either way.

   The 2-cells are implicit in any diagram called commutative.

   Yeah, that’s why I did the diagrams the way I did them. But I thought you had just been suggesting in #6 to make them explicit.

   But never mind, I guess we agree either way.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexMulling this over some more, I think there is a better way to describe dependent sums categorically in this style. The universal property we should be using is that $\sum_X A$ is the universal object equipped with a map $p_1$ to $X$ and a section $p_2$ of the pullback of the fibration $A\twoheadrightarrow X$ along this map. The pictures are hard to draw with instiki arrays, but here they are in quicklatex: * formation: <http://quicklatex.com/cache3/ql_1c81764c5c9e8040d29b987f7bf8d9c4_l3.png> * introduction: <http://quicklatex.com/cache3/ql_b15b695fe91cae98b53d5c8747d06f9c_l3.png> * elimination: <http://quicklatex.com/cache3/ql_a4014c37f882006d7254a62c72efcd6d_l3.png> * computation: <http://quicklatex.com/cache3/ql_00200297324152c6bcf2749f8322c4d9_l3.png>

    Mulling this over some more, I think there is a better way to describe dependent sums categorically in this style. The universal property we should be using is that $\sum_X A$ is the universal object equipped with a map $p_1$ to $X$ and a section $p_2$ of the pullback of the fibration $A\twoheadrightarrow X$ along this map. The pictures are hard to draw with instiki arrays, but here they are in quicklatex:

    • formation: http://quicklatex.com/cache3/ql_1c81764c5c9e8040d29b987f7bf8d9c4_l3.png
    • introduction: http://quicklatex.com/cache3/ql_b15b695fe91cae98b53d5c8747d06f9c_l3.png
    • elimination: http://quicklatex.com/cache3/ql_a4014c37f882006d7254a62c72efcd6d_l3.png
    • computation: http://quicklatex.com/cache3/ql_00200297324152c6bcf2749f8322c4d9_l3.png
11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012
    • (edited Oct 2nd 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks! I have added that into _[[dependent sum natural deduction - table]]_ Some questions: * In the formation rule would it be better to label the vertical arrow by $\in \mathcal{C}_{/A}$ than by $\in \mathcal{C}$? * How do I make _quicklatex_ display xymatrices? I did add \usepackage{xy}[all] in the quicklatex preamble, but that didn't help. * in the term introduction rule, strictly speaking $Q = X$ and $Q \stackrel{x}{\to} X $is $id_X$, right? Because the dependent term $a$ is simply a section of $A \to X$.

    Thanks! I have added that into dependent sum natural deduction - table

    Some questions:

    • In the formation rule would it be better to label the vertical arrow by $\in \mathcal{C}_{/A}$ than by $\in \mathcal{C}$?

    • How do I make quicklatex display xymatrices? I did add

      \usepackage{xy}[all]
      

      in the quicklatex preamble, but that didn’t help.

    • in the term introduction rule, strictly speaking $Q = X$ and $Q \stackrel{x}{\to} X$is $id_X$, right? Because the dependent term $a$ is simply a section of $A \to X$.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex* I'm disinclined, because I'd rather emphasize that the base object $X$ is part of the input data too. * the options come before the package name. * I think by analogy with what you wrote in the other tables, $Q$ represents the context $\Gamma$ in which the introduction rule is being applied.

    • I’m disinclined, because I’d rather emphasize that the base object $X$ is part of the input data too.

    • the options come before the package name.

    • I think by analogy with what you wrote in the other tables, $Q$ represents the context $\Gamma$ in which the introduction rule is being applied.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> the options come before the package name. Silly me. Thanks.

    the options come before the package name.

    Silly me. Thanks.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIt would be nice if quicklatex gave you the LaTeX error messages. (-:

    It would be nice if quicklatex gave you the LaTeX error messages. (-:

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeOct 17th 2012
    • (edited Oct 17th 2012)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexMike, those diagrams are excellent! In particular, you clearly separate the projection $p_1\colon \sum_X A \to X$ from the display map $A \twoheadrightarrow X$. These are often the same, but they play different roles.

    Mike, those diagrams are excellent!

    In particular, you clearly separate the projection $p_1\colon \sum_X A \to X$ from the display map $A \twoheadrightarrow X$. These are often the same, but they play different roles.

16. • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeOct 17th 2012
    • (edited Oct 17th 2012)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@Urs #11 first bullet point: It\'s $\in \mathcal{C}_{/X}$. One could well write $(A \in \mathcal{C}_{/X}) \Rightarrow (\sum_X A \in \mathcal{C})$, if the slice category is understood to consist only of display maps. (Later we abuse notation and use $A$ for the object in $\mathcal{C}$ rather than for the object in $\mathcal{C}_{/X}$. But if $A$ doesn\'t mean an object in $\mathcal{C}_{/X}$ rather than just an object in $\mathcal{C}$, then the notation $\sum_X A$ is the abuse.)

    @Urs #11 first bullet point:

    It's $\in \mathcal{C}_{/X}$. One could well write $(A \in \mathcal{C}_{/X}) \Rightarrow (\sum_X A \in \mathcal{C})$, if the slice category is understood to consist only of display maps. (Later we abuse notation and use $A$ for the object in $\mathcal{C}$ rather than for the object in $\mathcal{C}_{/X}$. But if $A$ doesn't mean an object in $\mathcal{C}_{/X}$ rather than just an object in $\mathcal{C}$, then the notation $\sum_X A$ is the abuse.)