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 13th 2010
   • (edited Sep 13th 2010)
   • PermaLink
   Author: Urs
   Format: MarkdownItexsince the discussion keeps coming up on the cat-theory mailing list and leads to repetition of questions and explanations, it is clear that we need a dedicated nLab page that gives a comprehensive discussion of the kind that next time the issue comes up on the cat-theory lst, you can just say "see here". I gather the relevant information is already available at various places on the nlab, but it looks like it would be worthwhile to have one dedicated page while the technical aspect of the issue is simple, it does clearly call for a bit of discussion.

   since the discussion keeps coming up on the cat-theory mailing list and leads to repetition of questions and explanations, it is clear that we need a dedicated nLab page that gives a comprehensive discussion of the kind that next time the issue comes up on the cat-theory lst, you can just say “see here”.

   I gather the relevant information is already available at various places on the nlab, but it looks like it would be worthwhile to have one dedicated page

   while the technical aspect of the issue is simple, it does clearly call for a bit of discussion.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSure, although since ‘type’ is a very broad term, many (if not most) type theories intended as a foundation of mathematics automatically have a notion of equality between elements of any given type. So I would say [[preset-theoretic definition of category]]. Anyway, I have to run off now, but I'll write it tonight if somebody else (Mike and David Roberts are qualified, I'm sure) doesn't beat me to it. It's just the ordinary defintion of [[enriched category]], specialised to the cartesian monoidal category $Set$, with a note that the collection of objects is a [[preset]]. But it deserves to be written out in full detail.

   Sure, although since ‘type’ is a very broad term, many (if not most) type theories intended as a foundation of mathematics automatically have a notion of equality between elements of any given type. So I would say preset-theoretic definition of category.

   Anyway, I have to run off now, but I’ll write it tonight if somebody else (Mike and David Roberts are qualified, I’m sure) doesn’t beat me to it. It’s just the ordinary defintion of enriched category, specialised to the cartesian monoidal category $Set$, with a note that the collection of objects is a preset. But it deserves to be written out in full detail.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexOn second thought, [[type-theoretic definition of category]] is probably fine. The essential shape of the definition is that it is based on dependent type theory. If the type theory has equality predicates on all types, so be it; ultimately that is irrelevant.

   On second thought, type-theoretic definition of category is probably fine. The essential shape of the definition is that it is based on dependent type theory. If the type theory has equality predicates on all types, so be it; ultimately that is irrelevant.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, Toby. > It's just the ordinary defintion of enriched category, specialised to the cartesian monoidal category Set, with a note that the collection of objects is a preset. Yes, the technical aspect is pretty trivial, but I was thinking it would be good the entry amplified a bit the maybe more philosophical issues of the kind that keep being discussed on the cat-theory list. Given that various people have asked about it while at the same time Bénabou and Joyal keep saying they don't see what the issue is, there seems to be need for some clarification.

   Thanks, Toby.

   It’s just the ordinary defintion of enriched category, specialised to the cartesian monoidal category Set, with a note that the collection of objects is a preset.

   Yes, the technical aspect is pretty trivial, but I was thinking it would be good the entry amplified a bit the maybe more philosophical issues of the kind that keep being discussed on the cat-theory list. Given that various people have asked about it while at the same time Bénabou and Joyal keep saying they don’t see what the issue is, there seems to be need for some clarification.

5. • CommentRowNumber5.
   • CommentAuthorUlrik
   • CommentTimeSep 14th 2010
   • (edited Sep 14th 2010)
   • PermaLink
   Author: Ulrik
   Format: TextI've added a definition to [[type-theoretic definition of category]], I hope it may serve as a basis for discussing philosophical issues. I didn't say anything about these, but I tried to take an approach that assumes very little about the foundations of the underlying type theory (e.g., it may or may not have equality predicates, and propositions may be types or not). But on the other hand I assumed a somewhat non-standard notation (borrowed from Epigram), hoping to make the definition easy to read. This is my first addition to the nLab, and I hope it is a welcome one!

   I've added a definition to type-theoretic definition of category, I hope it may serve as a basis for discussing philosophical issues. I didn't say anything about these, but I tried to take an approach that assumes very little about the foundations of the underlying type theory (e.g., it may or may not have equality predicates, and propositions may be types or not). But on the other hand I assumed a somewhat non-standard notation (borrowed from Epigram), hoping to make the definition easy to read.
   
   This is my first addition to the nLab, and I hope it is a welcome one!
6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThanks, Ulrik, that looks nice! You handled this bit very well: >I tried to take an approach that assumes very little about the foundations of the underlying type theory I changed one thing (besides cosmetic edits to use some iTeX features): I put the "$p\coloneq$" bits underneath the lines, since it seemed to me that this was more correct. For one thing, it matches having the "$p\colon$" bits under the lines in the other rules, and it's the only way that "$p\coloneq P$" appears (as in your explanation of the notation below), since a rule is not a proposition. (And it is more basic to name (proofs of) propositions, rather than rules, anyway.) Arguably, when they appear below the line, $\mathrm{left}\text{-}\mathrm{unit}$ and its friends should have subscripts on them, but then these are just more implicit parameters, right?

   Thanks, Ulrik, that looks nice! You handled this bit very well:

   I tried to take an approach that assumes very little about the foundations of the underlying type theory

   I changed one thing (besides cosmetic edits to use some iTeX features): I put the “$p\coloneq$” bits underneath the lines, since it seemed to me that this was more correct. For one thing, it matches having the “$p\colon$” bits under the lines in the other rules, and it’s the only way that “$p\coloneq P$” appears (as in your explanation of the notation below), since a rule is not a proposition. (And it is more basic to name (proofs of) propositions, rather than rules, anyway.) Arguably, when they appear below the line, $\mathrm{left}\text{-}\mathrm{unit}$ and its friends should have subscripts on them, but then these are just more implicit parameters, right?

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: Urs
   Format: MarkdownItexI added a link to this entry from [[category]]. Maybe one of you could add there a more helpful comment. I am not really sure how to put it.

   I added a link to this entry from category. Maybe one of you could add there a more helpful comment. I am not really sure how to put it.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI haven't actually looked at the content here yet, but perhaps the pages [[single-sorted definition of a category]] and [[type-theoretic definition of category]] should get together and decide whether there should be an article in front of "category". (-: My idiolect says there should be, but that could be wrong.

   I haven’t actually looked at the content here yet, but perhaps the pages single-sorted definition of a category and type-theoretic definition of category should get together and decide whether there should be an article in front of “category”. (-: My idiolect says there should be, but that could be wrong.

9. • CommentRowNumber9.
   • CommentAuthorUlrik
   • CommentTimeSep 14th 2010
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexI'm glad you like it, Toby! > I changed one thing ... I think I agree with this change, it is more standard at least. I also approve of your cosmetic changes. > Arguably, when they appear below the line, $\mathrm{left}\text{-}\mathrm{unit}$ and its friends should have subscripts on them, but then these are just more implicit parameters, right? Yes, though in most circumstances during a proof, I think current technology wouldn't be able to infer them. Of course, they should be inferable, and anyway it's not really relevant to the current topic. Regarding philosophical issues, the first thing that should be noted is that the defined type of categories cannot be a member of $\mathrm{Type}$ due to Girard's paradox (or some variant). I've added a stub for that to get things going.

   I’m glad you like it, Toby!

   I changed one thing …

   I think I agree with this change, it is more standard at least. I also approve of your cosmetic changes.

   Arguably, when they appear below the line, $\mathrm{left}\text{-}\mathrm{unit}$ and its friends should have subscripts on them, but then these are just more implicit parameters, right?

   Yes, though in most circumstances during a proof, I think current technology wouldn’t be able to infer them. Of course, they should be inferable, and anyway it’s not really relevant to the current topic.

   Regarding philosophical issues, the first thing that should be noted is that the defined type of categories cannot be a member of $\mathrm{Type}$ due to Girard’s paradox (or some variant). I’ve added a stub for that to get things going.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeSep 14th 2010
    • (edited Sep 14th 2010)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Urs >Maybe one of you could add there a more helpful comment. I redesigned the entire Definition section to show both definitions completely (although in ordinary set-theoretic language). @ Mike I think that there shouldn't be, but the redirects are there. @ Ulrik > ... Girard's paradox ... Right, that's size issues again.

    @ Urs

    Maybe one of you could add there a more helpful comment.

    I redesigned the entire Definition section to show both definitions completely (although in ordinary set-theoretic language).

    @ Mike

    I think that there shouldn’t be, but the redirects are there.

    @ Ulrik

    … Girard’s paradox …

    Right, that’s size issues again.