[-- Attachment #1.1: Type: text/plain, Size: 1098 bytes --] I want to get a general idea of peoples opinions when it comes to naming categories internal to HoTT. On the one hand I have seen, in the HoTT book for example, precategory and category being used where the latter has the map idtoiso being an equivalence. On the other hand I have seen people call these categories and univalent categories which is also fine. Now because we have Rezk completion every precategory is yearning to become a category, so some might argue that a distinction isn't necessery. I would argue that the HoTT book convention is infact more misleading as "precategory" there is really just the usual notion of category. And a univalent category is some nice structure we can add to it because we are working in HoTT. What are your thoughts and opinions on this? -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1393 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1204 bytes --] On Wed, 7 Nov 2018, at 10:03 AM, Ali Caglayan wrote: > Now because we have Rezk completion every precategory is yearning to become > a category, so some might argue that a distinction isn't necessery. I wouldn't say that. Yes, there is an adjunction between categories and precategories, but it's not an equivalence even in an ∞-categorical sense. In fact, following Ayala and Francis, you can think of a precategory as a category C equipped with the extra structure of a type X, and a surjective (i.e. -1-connected) morphism X → obj C. > What are your thoughts and opinions on this? Whatever notion ends up being called *category*, I would say it ought to at least be mapped to something that is (Quillen) equivalent to the usual notion of category through the simplicial set interpretation. That suggests categories should be univalent by default. Best, Paolo -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1430 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3190 bytes --] Hi, First, there are (at least) three mathematically important and useful types: precategories, strict (or set) categories (precategories with a set of objects), and (univalent) categories. I take as one main lesson from HoTT/UF that mathematical objects have types, and that the identity types should indicate the relevant notion of identity. The type of precategories is equivalent to that of type-flagged categories (categories together with a type O and a function from O to the objects of the category). (The equivalence is given by pulling back the category structure to get a precategory structure with O as the type of objects in one way, and taking the Rezk completion together with the object part of unit map in the other.) Two precategories are identified via an equivalence of the O-types and an equivalence of the categories, together with a witness that the square commutes. Two strict categories are identified via an isomorphism, and two (univalent) categories are identified via an equivalence. So I disagree that "precategory" is the usual notion of category: it can't be because the criterion of identity is different. But it's still a useful concept. I personally prefer to keep “category” for univalent precategory, as most often constructions on categories are meant to be well-defined up to equivalence of categories. In the category theory literature written in a set-theory metatheory where the distinction is not so clear, you can of course find plenty of uses of the word “category” where “strict category” is meant from a HoTT/UF point-of-view. The type of precategories as a common generalization of strict and univalent categories is, I think, a new concept to HoTT/UF. (Although infinity-groupoid flagged (infinity,1)-categories arose independently in homotopy theory; these could also be called (infinity,1)-precategories.) Cheers, Ulrik On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote: > > I want to get a general idea of peoples opinions when it comes to naming > categories internal to HoTT. > > On the one hand I have seen, in the HoTT book for example, precategory and > category being used where the latter has the map idtoiso being an > equivalence. > > On the other hand I have seen people call these categories and univalent > categories which is also fine. > > Now because we have Rezk completion every precategory is yearning to > become a category, so some might argue that a distinction isn't necessery. > I would argue that the HoTT book convention is infact more misleading as > "precategory" there is really just the usual notion of category. And a > univalent category is some nice structure we can add to it because we are > working in HoTT. > > What are your thoughts and opinions on this? > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3733 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3479 bytes --] Mine and Paolo's replies crossed, but of course I missed the condition that the function be surjective. On Wednesday, November 7, 2018 at 11:35:11 AM UTC+1, Ulrik Buchholtz wrote: > > Hi, > > First, there are (at least) three mathematically important and useful > types: precategories, strict (or set) categories (precategories with a set > of objects), and (univalent) categories. > > I take as one main lesson from HoTT/UF that mathematical objects have > types, and that the identity types should indicate the relevant notion of > identity. > > The type of precategories is equivalent to that of type-flagged categories > (categories together with a type O and a function from O to the objects of > the category). (The equivalence is given by pulling back the category > structure to get a precategory structure with O as the type of objects in > one way, and taking the Rezk completion together with the object part of > unit map in the other.) > > Two precategories are identified via an equivalence of the O-types and an > equivalence of the categories, together with a witness that the square > commutes. > > Two strict categories are identified via an isomorphism, and two > (univalent) categories are identified via an equivalence. > > So I disagree that "precategory" is the usual notion of category: it can't > be because the criterion of identity is different. But it's still a useful > concept. > > I personally prefer to keep “category” for univalent precategory, as most > often constructions on categories are meant to be well-defined up to > equivalence of categories. In the category theory literature written in a > set-theory metatheory where the distinction is not so clear, you can of > course find plenty of uses of the word “category” where “strict category” > is meant from a HoTT/UF point-of-view. The type of precategories as a > common generalization of strict and univalent categories is, I think, a new > concept to HoTT/UF. (Although infinity-groupoid flagged > (infinity,1)-categories arose independently in homotopy theory; these could > also be called (infinity,1)-precategories.) > > Cheers, > Ulrik > > On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote: >> >> I want to get a general idea of peoples opinions when it comes to naming >> categories internal to HoTT. >> >> On the one hand I have seen, in the HoTT book for example, precategory >> and category being used where the latter has the map idtoiso being an >> equivalence. >> >> On the other hand I have seen people call these categories and univalent >> categories which is also fine. >> >> Now because we have Rezk completion every precategory is yearning to >> become a category, so some might argue that a distinction isn't necessery. >> I would argue that the HoTT book convention is infact more misleading as >> "precategory" there is really just the usual notion of category. And a >> univalent category is some nice structure we can add to it because we are >> working in HoTT. >> >> What are your thoughts and opinions on this? >> > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4068 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1835 bytes --] Ulrik’s email nicely lays out the three key notions (pre-category, strict category, univalent category), and the argument for the Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning “univalent category” by default. For my part I lean the other way: I think it’s too radical to use “category” for a definition which doesn’t come out equivalent to the traditional definition under the naïve set interpretation (or under the addition of UIP to the type theory). Choosing terminology that actively clashes with traditional terminology makes it much harder to compare statements in HoTT with their classical analogues, and see what difference HoTT really makes to the development of topics. Based on that criterion, I strongly prefer taking category to mean “precategory”. A big payoff from this is that if you formalise something using “category ” to mean “precategory” in type theory without assuming UA, then you can read the result either as valid in HoTT, or (under the set-interpretation) as ordinary arguments in classical category theory, with all the terms meaning just what they traditionally would. Univalence of categories is an important and powerful property, but not an innocuous one; it changes the character of the resulting “category theory” in interesting ways. Making the restriction to univalent categories tacit is misleading to readers who aren’t fully “insiders”, and obscures understanding its effects. –p. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 2111 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2504 bytes --] I'm a bit confused by your message, Peter: HoTT doesn't have a naive set interpretation and is inconsistent with UIP, so I'm not sure how that should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine wrote: > > Ulrik’s email nicely lays out the three key notions (pre-category, strict > category, univalent category), and the argument for the > Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning > “univalent category” by default. > > For my part I lean the other way: I think it’s too radical to use > “category” for a definition which doesn’t come out equivalent to the > traditional definition under the naïve set interpretation (or under the > addition of UIP to the type theory). Choosing terminology that actively > clashes with traditional terminology makes it much harder to compare > statements in HoTT with their classical analogues, and see what difference > HoTT really makes to the development of topics. > > Based on that criterion, I strongly prefer taking category to mean > “precategory”. A big payoff from this is that if you formalise something > using “category ” to mean “precategory” in type theory without assuming UA, > then you can read the result either as valid in HoTT, or (under the > set-interpretation) as ordinary arguments in classical category theory, > with all the terms meaning just what they traditionally would. > > Univalence of categories is an important and powerful property, but not an > innocuous one; it changes the character of the resulting “category theory” > in interesting ways. Making the restriction to univalent categories tacit > is misleading to readers who aren’t fully “insiders”, and obscures > understanding its effects. > > –p. > > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2912 bytes --]

There is a paper to appear in TYPES 2017 postproceeding that discusses this from the old MLTT perspective http://staff.math.su.se/palmgren/7.pdf Erik Den 2018-11-07 kl. 12:43, skrev Ulrik Buchholtz: > I'm a bit confused by your message, Peter: HoTT doesn't have a naive set > interpretation and is inconsistent with UIP, so I'm not sure how that > should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) > > As I tried to say, I find that precategory is the novel concept, and > that both strict category and univalent category should be familiar to > category theorists. (They have a mental model for when one notion is > called for or the other, but we can make the distinction formal.) > > On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu > Lumsdaine wrote: > > Ulrik’s email nicely lays out the three key notions (pre-category, > strict category, univalent category), and the argument for the > Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” > meaning “univalent category” by default. > > For my part I lean the other way: I think it’s too radical to use > “category” for a definition which doesn’t come out equivalent to the > traditional definition under the naïve set interpretation (or under > the addition of UIP to the type theory). Choosing terminology that > actively clashes with traditional terminology makes it much harder > to compare statements in HoTT with their classical analogues, and > see what difference HoTT really makes to the development of topics. > > Based on that criterion, I strongly prefer taking category to mean > “precategory”. A big payoff from this is that if you formalise > something using “category ” to mean “precategory” in type theory > without assuming UA, then you can read the result either as valid in > HoTT, or (under the set-interpretation) as ordinary arguments in > classical category theory, with all the terms meaning just what they > traditionally would. > > Univalence of categories is an important and powerful property, but > not an innocuous one; it changes the character of the resulting > “category theory” in interesting ways. Making the restriction to > univalent categories tacit is misleading to readers who aren’t fully > “insiders”, and obscures understanding its effects. > > –p. > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 3216 bytes --] Let me add one more point: in agnostic type theory, we can't define the type of (Cauchy) real numbers, so we make do with the setoid of Cauchy sequences. Likewise, we can't define the type of (univalent) categories, so we make do with the 2-groupoid of precategories, equivalences and natural isomorphisms. In agnostic type theory we are both in setoid and higher groupoid hell. In set theory/extensional type theory, we can escape the setoid hell, but still have the higher groupoid hell, and in HoTT we can finally escape this particular family of infernos :) On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote: > > I'm a bit confused by your message, Peter: HoTT doesn't have a naive set > interpretation and is inconsistent with UIP, so I'm not sure how that > should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) > > As I tried to say, I find that precategory is the novel concept, and that > both strict category and univalent category should be familiar to category > theorists. (They have a mental model for when one notion is called for or > the other, but we can make the distinction formal.) > > On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu > Lumsdaine wrote: >> >> Ulrik’s email nicely lays out the three key notions (pre-category, strict >> category, univalent category), and the argument for the >> Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning >> “univalent category” by default. >> >> For my part I lean the other way: I think it’s too radical to use >> “category” for a definition which doesn’t come out equivalent to the >> traditional definition under the naïve set interpretation (or under the >> addition of UIP to the type theory). Choosing terminology that actively >> clashes with traditional terminology makes it much harder to compare >> statements in HoTT with their classical analogues, and see what difference >> HoTT really makes to the development of topics. >> >> Based on that criterion, I strongly prefer taking category to mean >> “precategory”. A big payoff from this is that if you formalise something >> using “category ” to mean “precategory” in type theory without assuming UA, >> then you can read the result either as valid in HoTT, or (under the >> set-interpretation) as ordinary arguments in classical category theory, >> with all the terms meaning just what they traditionally would. >> >> Univalence of categories is an important and powerful property, but not >> an innocuous one; it changes the character of the resulting “category >> theory” in interesting ways. Making the restriction to univalent >> categories tacit is misleading to readers who aren’t fully “insiders”, and >> obscures understanding its effects. >> >> –p. >> >> -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3741 bytes --]

Setoid hell? This sounds like a sermon ... :-) I think the critique needs to be a little more specific. Den 2018-11-07 kl. 12:51, skrev Ulrik Buchholtz: > Let me add one more point: in agnostic type theory, we can't define the > type of (Cauchy) real numbers, so we make do with the setoid of Cauchy > sequences. Likewise, we can't define the type of (univalent) categories, > so we make do with the 2-groupoid of precategories, equivalences and > natural isomorphisms. > > In agnostic type theory we are both in setoid and higher groupoid hell. > In set theory/extensional type theory, we can escape the setoid hell, > but still have the higher groupoid hell, and in HoTT we can finally > escape this particular family of infernos :) > > On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote: > > I'm a bit confused by your message, Peter: HoTT doesn't have a naive > set interpretation and is inconsistent with UIP, so I'm not sure how > that should guide us. (Maybe if we're working in good old > (agnostic?) MLTT?) > > As I tried to say, I find that precategory is the novel concept, and > that both strict category and univalent category should be familiar > to category theorists. (They have a mental model for when one notion > is called for or the other, but we can make the distinction formal.) > > On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu > Lumsdaine wrote: > > Ulrik’s email nicely lays out the three key notions > (pre-category, strict category, univalent category), and the > argument for the Ahrens–Kapulkin–Shulman / HoTT book > terminology, with “category” meaning “univalent category” by > default. > > For my part I lean the other way: I think it’s too radical to > use “category” for a definition which doesn’t come out > equivalent to the traditional definition under the naïve set > interpretation (or under the addition of UIP to the type > theory). Choosing terminology that actively clashes with > traditional terminology makes it much harder to compare > statements in HoTT with their classical analogues, and see what > difference HoTT really makes to the development of topics. > > Based on that criterion, I strongly prefer taking category to > mean “precategory”. A big payoff from this is that if you > formalise something using “category ” to mean “precategory” in > type theory without assuming UA, then you can read the result > either as valid in HoTT, or (under the set-interpretation) as > ordinary arguments in classical category theory, with all the > terms meaning just what they traditionally would. > > Univalence of categories is an important and powerful property, > but not an innocuous one; it changes the character of the > resulting “category theory” in interesting ways. Making the > restriction to univalent categories tacit is misleading to > readers who aren’t fully “insiders”, and obscures understanding > its effects. > > –p. > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1096 bytes --] On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: > > Setoid hell? This sounds like a sermon ... :-) > This theological aspect seems to be an attribute of constructive mathematics. We also have the Limited Principle of Omniscience. Both the Setoid Hell was created and LPO was named by Bishop. Perhaps this is justified by his very own name. But seriously, I would like to have the terminology for the various types of categories settled and agreed among ourselves. I agree with the mathematical argument given by Ulrik. I sympathize with Peter's argument, which tries to avoid confusion, but I think in the long term it may cause even more confusion. Maybe Ulrik's remarks should be added to the HoTT Book and blogged at https://homotopytypetheory.org/blog/ Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1498 bytes --]

Den 2018-11-07 kl. 13:21, skrev Martín Hötzel Escardó: > > > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: > > Setoid hell? This sounds like a sermon ... :-) > > > This theological aspect seems to be an attribute of constructive > mathematics. We also have the Limited Principle of Omniscience. Both the > Setoid Hell was created and LPO was named by Bishop. Perhaps this is > justified by his very own name. Bishop seem rather antitheological about mathematics in his Manifesto. Anyway. > > But seriously, I would like to have the terminology for the various > types of categories settled and agreed among ourselves. I agree with the > mathematical argument given by Ulrik. I sympathize with Peter's > argument, which tries to avoid confusion, but I think in the long term > it may cause even more confusion. Maybe Ulrik's remarks should be added > to the HoTT Book and blogged at https://homotopytypetheory.org/blog/ From http://staff.math.su.se/palmgren/7.pdf: "In conclusion, the notion of univalent category is too restrictive to cover many familiar examples. H-category is generalization of precategory and is a convenient version of E- category with equality on objects. The notion of E-category is still more general as shown here." > Martin > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

We also have a wiki of course: https://ncatlab.org/homotopytypetheory/show/HomePage On Wed, Nov 7, 2018 at 1:21 PM Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > > > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: >> >> Setoid hell? This sounds like a sermon ... :-) > > > This theological aspect seems to be an attribute of constructive mathematics. We also have the Limited Principle of Omniscience. Both the Setoid Hell was created and LPO was named by Bishop. Perhaps this is justified by his very own name. > > But seriously, I would like to have the terminology for the various types of categories settled and agreed among ourselves. I agree with the mathematical argument given by Ulrik. I sympathize with Peter's argument, which tries to avoid confusion, but I think in the long term it may cause even more confusion. Maybe Ulrik's remarks should be added to the HoTT Book and blogged at https://homotopytypetheory.org/blog/ > > Martin > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1693 bytes --] I wrote the "category theory in HoTT" articles on the wiki. They are nothing more than what is already in the book. Part of the reason for this question is to make sure there is some agreement on what I am writing. On Wednesday, 7 November 2018 13:03:03 UTC, Bas Spitters wrote: > > We also have a wiki of course: > https://ncatlab.org/homotopytypetheory/show/HomePage > On Wed, Nov 7, 2018 at 1:21 PM Martín Hötzel Escardó > <escardo...@gmail.com <javascript:>> wrote: > > > > > > > > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: > >> > >> Setoid hell? This sounds like a sermon ... :-) > > > > > > This theological aspect seems to be an attribute of constructive > mathematics. We also have the Limited Principle of Omniscience. Both the > Setoid Hell was created and LPO was named by Bishop. Perhaps this is > justified by his very own name. > > > > But seriously, I would like to have the terminology for the various > types of categories settled and agreed among ourselves. I agree with the > mathematical argument given by Ulrik. I sympathize with Peter's argument, > which tries to avoid confusion, but I think in the long term it may cause > even more confusion. Maybe Ulrik's remarks should be added to the HoTT Book > and blogged at https://homotopytypetheory.org/blog/ > > > > Martin > > > > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3260 bytes --]

It would appear to me as natural to call "categories" the most general notion and "univalent" those ones which validate the univalence axiom. In any case the word "category" should not imply univalence. But there is a point that one might call the most general notion "precategory" and "categories" those precategories whose hom types validate UIP, i.e. are sets. But then univalent categories are not categories but just precategories. Why not call the general notion "\infty-category" as usual? Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 4319 bytes --] I'm a bit confused by your message, Peter: HoTT doesn't have a naive set interpretation and is inconsistent with UIP, so I'm not sure how that should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) This is too clever! If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so. Hence I think the terminology category / univalent category is preferable. This also maintains the traditional wisdom that categories (with trivial ie.e propositional homsets) correspond to preorders. We may add that univalent categories correspond to partial orders. And yes indeed there is something wrong with preorders because they have equality and equivalence and hence it is better to have a preorder. The same holds for categories, you have both equality and isomorphism and hence it is better to have a univalent category. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Ulrik Buchholtz <ulrikbuchholtz@gmail.com> Date: Wednesday, 7 November 2018 at 11:44 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine wrote: Ulrik’s email nicely lays out the three key notions (pre-category, strict category, univalent category), and the argument for the Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning “univalent category” by default. For my part I lean the other way: I think it’s too radical to use “category” for a definition which doesn’t come out equivalent to the traditional definition under the naïve set interpretation (or under the addition of UIP to the type theory). Choosing terminology that actively clashes with traditional terminology makes it much harder to compare statements in HoTT with their classical analogues, and see what difference HoTT really makes to the development of topics. Based on that criterion, I strongly prefer taking category to mean “precategory”. A big payoff from this is that if you formalise something using “category ” to mean “precategory” in type theory without assuming UA, then you can read the result either as valid in HoTT, or (under the set-interpretation) as ordinary arguments in classical category theory, with all the terms meaning just what they traditionally would. Univalence of categories is an important and powerful property, but not an innocuous one; it changes the character of the resulting “category theory” in interesting ways. Making the restriction to univalent categories tacit is misleading to readers who aren’t fully “insiders”, and obscures understanding its effects. –p. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 9430 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2178 bytes --] On Wed, Nov 7, 2018 at 12:43 PM Ulrik Buchholtz <ulrikbuchholtz@gmail.com> wrote: > I'm a bit confused by your message, Peter: HoTT doesn't have a naive set > interpretation and is inconsistent with UIP, so I'm not sure how that > should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) > Yep, I indeed meant “agnostic” MLTT — in particular, without univalence (or roughly-equivalent things like the glue-types of cubical type theory). There are lots of motivations for working over that as far as possible: baking univalence into material where it’s not really required feels like when classical mathematicians make use of AC for no real advantage. As I tried to say, I find that precategory is the novel concept, and that > both strict category and univalent category should be familiar to category > theorists. (They have a mental model for when one notion is called for or > the other, but we can make the distinction formal.) > I would argue both are familiar to traditional category theorists. It’s not unusual to make use of, for instance, the small model for FinSet where the set of objects is taken as N — call this FinSet_N, say. Category theorists would certainly say that there’s a difference in character between FinSet_N and FinSet itself: FinSet_N is small; and I think they would also agree that they’re conscious informally of an extra character FinSet has, which in HoTT can be precisely expressed as its univalence. But do you really think they don’t consider FinSet_N to be a category?? I find that very hard to believe: I am pretty sure that most traditional category theorists would consider FinSet_N a category without any doubt at all, which really seems to imply that the standard concept of category is more like “precategory” than “univalent category”. –p. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 2942 bytes --]

Something that only satisfies the axioms of a category but whose homs are not sets I would call a "wild category". So yes a category needs to have homsets otherwise you have to give it a number. And -1-categories already have a name they are called preorders. I think the interesting notion for HoTT are categories whose Homs are types and which fullfill all the coherence conditions, i.e. they correspond to (\infty,1)-categories. Nicolai and Paolo gave a definition of univalent (\infty,1)-cats in 2-level HoTT as "complete Segal types". From this one can aslo derive non-univalent (\inft,1)-cats but in this case it is easier to define the univalent version because then you don't have to deal with degeneracies. Thorsten On 07/11/2018, 13:53, "homotopytypetheory@googlegroups.com on behalf of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of streicher@mathematik.tu-darmstadt.de> wrote: It would appear to me as natural to call "categories" the most general notion and "univalent" those ones which validate the univalence axiom. In any case the word "category" should not imply univalence. But there is a point that one might call the most general notion "precategory" and "categories" those precategories whose hom types validate UIP, i.e. are sets. But then univalent categories are not categories but just precategories. Why not call the general notion "\infty-category" as usual? Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1604 bytes --] On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote: > > As I tried to say, I find that precategory is the novel concept, and that > both strict category and univalent category should be familiar to category > theorists. (They have a mental model for when one notion is called for or > the other, but we can make the distinction formal.) > > > This is too clever! > > > > If you just transcribe the traditional definition of a category in type > theory you end up with what in the HoTT book is called precategory. This is > confusing for the non-expert even though you can justify why it should be > so. > No, you get the notion of a strict category, which in some sense is all that you directly have in set theory. (To get the (2,1)-category of univalent categories, you take the homotopy (2,1)-category of the folk model structure on the category(?!) of strict categories.) As I said before, the notion of strict category is useful, and encompasses the examples that Erik was missing from univalent categories. But from a HoTT/UF point of view, the notion of strict category has the drawback that you cannot get a strict category of sets (or groups or…) without assuming the axiom (a homotopical taboo) that sets cover. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2176 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1770 bytes --] On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbuchholtz@gmail.com> wrote: > On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch > wrote: >> >> As I tried to say, I find that precategory is the novel concept, and that >> both strict category and univalent category should be familiar to category >> theorists. (They have a mental model for when one notion is called for or >> the other, but we can make the distinction formal.) >> >> >> This is too clever! >> >> >> >> If you just transcribe the traditional definition of a category in type >> theory you end up with what in the HoTT book is called precategory. This is >> confusing for the non-expert even though you can justify why it should be >> so. >> > > No, you get the notion of a strict category, which in some sense is all > that you directly have in set theory. > No in turn: you can arguably get either strict categories, or precategories, or what Thorsten dubbed “wild categories” above, since “set” in set theory is the (naïve) interpretation of both “set” and “type”. (Just as when you transcribe classical definitions in a constructive setting, you sometimes want to read “predicate” just as “predicate” and other times as “decidable predicate” — all predicates are decidable classically, but that doesn’t mean that their constructive transcription should include “decidable” by default.) –p. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 2667 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2243 bytes --] On Wednesday, November 7, 2018 at 3:05:44 PM UTC+1, Peter LeFanu Lumsdaine wrote: > > Yep, I indeed meant “agnostic” MLTT — in particular, without univalence > (or roughly-equivalent things like the glue-types of cubical type theory). > There are lots of motivations for working over that as far as possible: > baking univalence into material where it’s not really required feels like > when classical mathematicians make use of AC for no real advantage. > I'm in some respects sympathetic to this. We just have to be aware that working in agnostic type theory leaves us with a burden of mentally/manually handling the relevant notions of identity because the identity types cannot be relied upon. But do you really think they don’t consider FinSet_N to be a category?? I >> find that very hard to believe: I am pretty sure that most traditional >> category theorists would consider FinSet_N a category without any doubt at >> all, which really seems to imply that the standard concept of category is >> more like “precategory” than “univalent category”. >> > Well, FinSet_N presents FinSet and we often elide the difference between an object and a presentation for it, but we do so at our own peril. Traditionally, all categories are presented by a strict category, but traditional category theorists context-switch easily between strict and univalent categories (using heuristics about “evil”–there we go with the preaching again, sorry!). I'm beginning to despair for ever using the word “category” again without a modifier. The notion of “precategory” is pretty weird in the standard model: Why should the notion of an infinity-groupoid with a family of hom-sets be the sanctified notion?! Of course it turns out to be a useful notion, just like group presentations are useful. But group theory is about groups, not group presentations. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3210 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2948 bytes --] Strict cats are no good because the first example of a category, the category of sets isn’t one. And we always say homSETS but not sets of objects (ok this is mainly for size but the two are not unrelated). Btw, there are strict univalent cats but they are quite rare… Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Ulrik Buchholtz <ulrikbuchholtz@gmail.com> Date: Wednesday, 7 November 2018 at 14:14 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote: As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) This is too clever! If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so. No, you get the notion of a strict category, which in some sense is all that you directly have in set theory. (To get the (2,1)-category of univalent categories, you take the homotopy (2,1)-category of the folk model structure on the category(?!) of strict categories.) As I said before, the notion of strict category is useful, and encompasses the examples that Erik was missing from univalent categories. But from a HoTT/UF point of view, the notion of strict category has the drawback that you cannot get a strict category of sets (or groups or…) without assuming the axiom (a homotopical taboo) that sets cover. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 7576 bytes --]

What one calls a category should be a set in the HoTT sense, i.e. validate UIP, but not a set in the sense of size. Every deviation from that should be signalled by some adjectives or prefixes. That reflects the practice in category theory. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Meinst Du dass die Homs sets sind, oder? Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein und HSet). T. On 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on behalf of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of streicher@mathematik.tu-darmstadt.de> wrote: What one calls a category should be a set in the HoTT sense, i.e. validate UIP, but not a set in the sense of size. Every deviation from that should be signalled by some adjectives or prefixes. That reflects the practice in category theory. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Sorry, I meant to reply only to Thomas. That explains the language which is not the internal language of some category... T On 07/11/2018, 16:55, "homotopytypetheory@googlegroups.com on behalf of Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of Thorsten.Altenkirch@nottingham.ac.uk> wrote: Meinst Du dass die Homs sets sind, oder? Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein und HSet). T. On 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on behalf of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of streicher@mathematik.tu-darmstadt.de> wrote: What one calls a category should be a set in the HoTT sense, i.e. validate UIP, but not a set in the sense of size. Every deviation from that should be signalled by some adjectives or prefixes. That reflects the practice in category theory. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 3866 bytes --] I also agree with Mike and Ulrik. I feel like the example of categories is the perfect opportunity to explain to someone who is interested in HoTT *why* there is a version of the definition that we prefer, *why* it is different from the notion they may be familiar with and *why*, in my humble opinion, it is an improvement. On Wed, Nov 7, 2018 at 5:56 PM Thorsten Altenkirch < Thorsten.Altenkirch@nottingham.ac.uk> wrote: > Sorry, I meant to reply only to Thomas. That explains the language which > is not the internal language of some category... > > T > > On 07/11/2018, 16:55, "homotopytypetheory@googlegroups.com on behalf of > Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of > Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > Meinst Du dass die Homs sets sind, oder? > > Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere > erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein > und HSet). > > T. > > On 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on behalf > of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of > streicher@mathematik.tu-darmstadt.de> wrote: > > What one calls a category should be a set in the HoTT sense, > i.e. validate UIP, but not a set in the sense of size. > > Every deviation from that should be signalled by some adjectives or > prefixes. That reflects the practice in category theory. > > Thomas > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 5567 bytes --]

On Wed, Nov 7, 2018 at 6:05 AM Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com> wrote: >> As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) > > I would argue both are familiar to traditional category theorists. It’s not unusual to make use of, for instance, the small model for FinSet where the set of objects is taken as N — call this FinSet_N, say. Category theorists would certainly say that there’s a difference in character between FinSet_N and FinSet itself: FinSet_N is small; and I think they would also agree that they’re conscious informally of an extra character FinSet has, which in HoTT can be precisely expressed as its univalence. > > But do you really think they don’t consider FinSet_N to be a category?? I find that very hard to believe: I am pretty sure that most traditional category theorists would consider FinSet_N a category without any doubt at all, which really seems to imply that the standard concept of category is more like “precategory” than “univalent category”. This is a really interesting question. Traditional category theorists do of course consider FinSet_N to be a category; in particular, it *is* a category according to the definition of "category" in ZFC. One could view this situation as analogous to that of truncated and untruncated Sigmas. When formalizing mathematics in ZFC, there are no untruncated Sigmas. When formalizing mathematics in MLTT, there are no truncated Sigmas. But when formalizing mathematics in HoTT, we have both truncated and untruncated Sigmas. We used to ask the question "when formalizing mathematics in HoTT, should the quantifier 'there exists' be interpreted as a truncated Sigma or an untruncated Sigma?" (This is what led to the somewhat-awkward use of the word "merely" in the book.) But more recently a number of us seem to believe that that's the wrong question, as it presupposes that mathematics has *already* been interpreted into first-order logic, which destroys the *natural* distinction between truncated and untruncated Sigma. Instead we should directly interpret mathematics into HoTT, choosing truncated and untruncated Sigmas as appropriate for the mathematics, without feeling the need to pass through first-order logic. Similarly, when formalizing category theory in ZFC, there are no univalent categories, only strict ones; thus we have to carefully ignore the strictness when working with categories that "should" be univalent. I don't know if there is any foundational theory in which *all* categories are univalent. But when formalizing category theory in HoTT, we have both; and so one might argue that it's wrong to ask whether the word 'category' should refer to strict categories or univalent ones, and instead we should use one or the other as appropriate for the mathematics -- and thus the general word 'category' should refer to something that includes both of them, such as precategories. Is that roughly the point you are making, Peter? I can't deny that there is something to this argument. However, I have two objections to it, or at least to its conclusion. The first is that the analogy breaks down in the following way. The awkwardness of formalizing mathematics in first-order logic comes from *conflating* truncated and untruncated Sigmas. Thus, the problem is solved in HoTT by simply distinguishing them. However, the awkwardness of formalizing category theory in ZFC comes not merely from conflating strict categories with univalent ones, but because doing category theory with strict categories is *intrinsically* awkward, whereas most applications of category theory involve only univalent categories (or more precisely, categories that *should* be univalent), so that awkwardness shouldn't be necessary. I think this is Eric's point: doing category theory with univalent categories is *nicer* than doing it in ZFC, whereas doing category theory with strict categories is *no better* than doing it in ZFC. Why wouldn't we want to emphasize one of the "selling points" of HoTT in our terminology? The strict categories are still there whenever we need them, but giving them a slightly derogatory red-herring adjective is appropriate because they are, for the most part, less well-behaved, and not what the subject of "category theory" is primarily about. My second objection is to the jump from "something that includes both strict and univalent categories" to "precategories". One can argue that traditional category theorists have a notion of "category" that includes both strict categories and univalent categories, but I would argue that their notion does *not* include precategories *other* than strict and univalent ones; instead it is something more like the "union" of strict categories and univalent categories, which is much smaller than the world of precategories. As evidence, I suggest that to a traditional category theorist, the statement "a fully faithful and essentially surjective functor is a (strong) equivalence" is either "just true", "becomes true if you set up the definitions correctly", or "becomes true if you assume the axiom of choice" (depending on the particular category theorist's attitude towards the axiom of choice). In HoTT, this statement for univalent categories is "just true" without any axiom of choice (one way in which doing category theory with univalent categories is nicer), while this statement for strict categories is related to the axiom of choice in exactly the same way as it is in ZFC. But this statement for general precategories is *just false*!! This is easy to see: let Y be any type, considered as a univalent groupoid, let f : X -> Y be any surjection of types, and make X into a precategory in the unique way such that f becomes a fully faithful functor. Then f is also essentially surjective, but for it to be an equivalence the surjection f must have a section; and there are plenty of surjections of types that have no section, such as the inclusion of the basepoint of S^1. So precategories are really weird, and if we define the word "category" to mean "precategory" then category theorists learning about HoTT will see things like this and react "whoa, category theory in HoTT is really weird" -- whereas the correct reaction (when using univalent categories) is "whoa, category theory in HoTT is really awesome"! Moreover, as Ulrik pointed out, there is a notion in traditional (higher) category theory that (under the standard interpretations of HoTT) does coincide with precategories. They're called "flagged categories": https://arxiv.org/abs/1801.08973. In particular, they are *not* called just "categories"! This to me is additional strong evidence that the traditional category theorist's notion of "category" does not include precategories. So if we in HoTT used "category" to mean "precategory", then we would actually be *renaming* something that already exists in traditional mathematics, in a highly confusing way. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

On Wed, Nov 7, 2018 at 7:55 AM Michael Shulman <shulman@sandiego.edu> wrote: > I doubt there is *any* > choice of terminology for plain MLTT without UA *or* UIP that is > sensible in that it can be specialized to the right terminology upon > the addition of either of these two inconsistent axioms. Well, with tongue slightly in cheek, here is one such definition: a category is a precategory C such that (if UA holds then C is univalent). (-: -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Thorsten asked why I prefer to have strict equality on categories. The answer is that one needs it in category theory typically when speaking about Grothendieck fibrations. And the latter is most useful in many contexts in particular when understanding geometric morphisms. This by the way also extends to Grothendieck fibrations in quasicategories as in Joyal and Lurie's accounts. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

There’s a (2-categorical) characterization of fibrations due to Ross Street that I like that works well in the (∞,1)-categorical context. In quasi-categories this captures the class of maps that Joyal/Lurie call “cartesian fibrations” but this definition can be used for other models of (∞,1)-categories as well. A functor p : E —> B between (∞,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 —> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible). A functor p : E —> B between (∞,1)-categories is a discrete cartesian fibration (aka right fibration) if the corresponding functor p^2 : E^2 —> B/p is an equivalence. Here E^2 is the (∞,1)-category of arrows in E (the cotensor with the walking arrow category 2) while B/p is a pullback of B^2 along p : E —> B in the codomain variable. If p : E —> B is an isofibration (in models, this is the notion of fibration in the corresponding model category; eg the Joyal model structure for quasi-categories) then p^2 : E^2 —> B/p is also an isofibration and you can modify the right adjoint right inverse so that the right adjoint is a strict section and the counit is an identity. This can be technically convenient — the adjunction is now a fibered adjunction and can be pulled back more easily — but strict equality doesn’t feel necessary to me in this context. Best, Emily — Assistant Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl > On Nov 8, 2018, at 6:58 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > > Thorsten asked why I prefer to have strict equality on categories. > The answer is that one needs it in category theory typically when > speaking about Grothendieck fibrations. > And the latter is most useful in many contexts in particular when > understanding geometric morphisms. This by the way also extends to > Grothendieck fibrations in quasicategories as in Joyal and Lurie's > accounts. > > Thomas > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

I should have added references. Street’s original papers are here: “Fibrations and Yoneda’s lemma in a 2-category" https://link.springer.com/chapter/10.1007%2FBFb0063102 “Fibrations in bicategories" http://www.numdam.org/article/CTGDC_1980__21_2_111_0.pdf For a rough draft of the (∞,1)-categorical story, see Chapter 5 of this: http://www.math.jhu.edu/~eriehl/elements.pdf Best, Emily — Assistant Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl > On Nov 8, 2018, at 7:23 AM, Emily Riehl <eriehl@math.jhu.edu> wrote: > > > There’s a (2-categorical) characterization of fibrations due to Ross Street that I like that works well in the (∞,1)-categorical context. In quasi-categories this captures the class of maps that Joyal/Lurie call “cartesian fibrations” but this definition can be used for other models of (∞,1)-categories as well. > > A functor p : E —> B between (∞,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 —> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible). > > A functor p : E —> B between (∞,1)-categories is a discrete cartesian fibration (aka right fibration) if the corresponding functor p^2 : E^2 —> B/p is an equivalence. > > Here E^2 is the (∞,1)-category of arrows in E (the cotensor with the walking arrow category 2) while B/p is a pullback of B^2 along p : E —> B in the codomain variable. > > If p : E —> B is an isofibration (in models, this is the notion of fibration in the corresponding model category; eg the Joyal model structure for quasi-categories) then p^2 : E^2 —> B/p is also an isofibration and you can modify the right adjoint right inverse so that the right adjoint is a strict section and the counit is an identity. This can be technically convenient — the adjunction is now a fibered adjunction and can be pulled back more easily — but strict equality doesn’t feel necessary to me in this context. > > Best, > Emily > > — > Assistant Professor, Dept. of Mathematics > Johns Hopkins University > www.math.jhu.edu/~eriehl > >> On Nov 8, 2018, at 6:58 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: >> >> >> Thorsten asked why I prefer to have strict equality on categories. >> The answer is that one needs it in category theory typically when >> speaking about Grothendieck fibrations. >> And the latter is most useful in many contexts in particular when >> understanding geometric morphisms. This by the way also extends to >> Grothendieck fibrations in quasicategories as in Joyal and Lurie's >> accounts. >> >> Thomas >> >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Dear Emily, thanks for the various references. I was aware of Street's generalization which is obtained from Grothendieck fibrations by closing up under categorical equivalences. But when one works with fibrations P : XX -> BB then it is intrinsic to have have reindexing functors u^* : P(I) -> P(J) for all u : J -> I in the base. And these one doesn't have in case of Street fibrations. For me Grothendieck fibrations are a most useful tool for 1) categorical logic 2) category theory over toposes or even more general base categories 3) conceptual understanding of geometric morphisms and properties of them and there the stronger notion of Grothendieck is indispensible. For Street fibrations fibers over isomorphic objects need not be equivalent anymore. That appears to me as counter intuitive. But, well, speaking about fibers is evil anyway. Thomas PS (1) Admittedly, in HoTT one needs fibrations less since one has universes available. If I had to defense the HoTT view I would say that fibrations are meaningless and they were used by the old category theorists only because they lacked universes. (2) In ordinary category theory, at least in topos theory, speaking about internal categories is very important. I guess that is an eval notion because it is built on equality of objects. Is there something like an "internal quasicat"? -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Actually, you don't need strict equality on categories to talk about strict Grothendieck fibrations in type theory: https://ncatlab.org/nlab/show/displayed+category On Thu, Nov 8, 2018 at 3:58 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > Thorsten asked why I prefer to have strict equality on categories. > The answer is that one needs it in category theory typically when > speaking about Grothendieck fibrations. > And the latter is most useful in many contexts in particular when > understanding geometric morphisms. This by the way also extends to > Grothendieck fibrations in quasicategories as in Joyal and Lurie's > accounts. > > Thomas > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Hi Thomas, two answers: the first is that in this particular case one doesn't need strict equality because one can present this as an indexed structure in type theory, e.g. assume as given a category C then a fibration F is a structure with the following components (here I assume that the base cat C is given by objects |C|, morphisms C(_,_) and so on. |F| : |C| -> U Fm : C(x,y) -> |F|(x) -> |F|(y) -> U id_F : Fm id a a comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c coe : C(x,y) -> |F|(y) -> |F|(x) coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a) The 2nd answer is that this is not always possible and the most well known example are semi-simplicial types. In this case we can produce indexed structures for all finite approximations but we can't generate the approximations in a uniform way (the question is actually an open problem). However, you don't want to force your categories to be struct but you want to be able to talk about your univalent, non-strict categories from a strict metatheoretic perspective. This can be realized by a 2-level type theory as for example explained in our paper [1] http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf Cheers, Thorsten [1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561, author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus}, title ={{Extending Homotopy Type Theory with Strict Equality}}, booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages ={21:1--21:17}, series ={Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN ={978-3-95977-022-4}, ISSN ={1868-8969}, year ={2016}, volume ={62}, editor ={Jean-Marc Talbot and Laurent Regnier}, publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address ={Dagstuhl, Germany}, URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561}, URN ={urn:nbn:de:0030-drops-65612}, doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21}, annote ={Keywords: homotopy type theory, coherences, strict equality, homotopy type system} } On 08/11/2018, 11:58, "Thomas Streicher" <streicher@mathematik.tu-darmstadt.de> wrote: >Thorsten asked why I prefer to have strict equality on categories. >The answer is that one needs it in category theory typically when >speaking about Grothendieck fibrations. >And the latter is most useful in many contexts in particular when >understanding geometric morphisms. This by the way also extends to >Grothendieck fibrations in quasicategories as in Joyal and Lurie's >accounts. > >Thomas > > This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

> A functor p : E ???> B between (???,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 ???> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible). That's not the definition on the nLab nor is it the one in Lurie and also not in Joyal's writings. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Sorry, I was to quick pressing send. We need the category to have homsets C : |C| -> |C| -> Set which means that the equations of a category are propositional. Similar we need to say Fm : C(x,y) -> |F|(x) -> |F|(y) -> Set and add fibred id and composition and the laws (again propositional). Thorsten On 08/11/2018, 16:01, "homotopytypetheory@googlegroups.com on behalf of Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of Thorsten.Altenkirch@nottingham.ac.uk> wrote: >Hi Thomas, > >two answers: the first is that in this particular case one doesn't need >strict equality because one can present this as an indexed structure in >type theory, e.g. assume as given a category C then a fibration F is a >structure with the following components (here I assume that the base cat C >is given by objects |C|, morphisms C(_,_) and so on. > >|F| : |C| -> U >Fm : C(x,y) -> |F|(x) -> |F|(y) -> U >id_F : Fm id a a >comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c >coe : C(x,y) -> |F|(y) -> |F|(x) >coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a) > >The 2nd answer is that this is not always possible and the most well known >example are semi-simplicial types. In this case we can produce indexed >structures for all finite approximations but we can't generate the >approximations in a uniform way (the question is actually an open >problem). However, you don't want to force your categories to be struct >but you want to be able to talk about your univalent, non-strict >categories from a strict metatheoretic perspective. This can be realized >by a 2-level type theory as for example explained in our paper [1] >http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf > >Cheers, > >Thorsten > >[1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561, >author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus}, >title ={{Extending Homotopy Type Theory with Strict Equality}}, >booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL >2016)}, >pages ={21:1--21:17}, >series ={Leibniz International Proceedings in Informatics (LIPIcs)}, >ISBN ={978-3-95977-022-4}, >ISSN ={1868-8969}, >year ={2016}, >volume ={62}, >editor ={Jean-Marc Talbot and Laurent Regnier}, >publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, >address ={Dagstuhl, Germany}, >URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561}, >URN ={urn:nbn:de:0030-drops-65612}, >doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21}, >annote ={Keywords: homotopy type theory, coherences, strict equality, >homotopy type system} >} > > > > > >On 08/11/2018, 11:58, "Thomas Streicher" ><streicher@mathematik.tu-darmstadt.de> wrote: > >>Thorsten asked why I prefer to have strict equality on categories. >>The answer is that one needs it in category theory typically when >>speaking about Grothendieck fibrations. >>And the latter is most useful in many contexts in particular when >>understanding geometric morphisms. This by the way also extends to >>Grothendieck fibrations in quasicategories as in Joyal and Lurie's >>accounts. >> >>Thomas >> >> > > > > >This message and any attachment are intended solely for the addressee >and may contain confidential information. If you have received this >message in error, please contact the sender and delete the email and >attachment. > >Any views or opinions expressed by the author of this email do not >necessarily reflect the views of the University of Nottingham. Email >communications with the University of Nottingham may be monitored >where permitted by law. > > > > >-- >You received this message because you are subscribed to the Google Groups >"Homotopy Type Theory" group. >To unsubscribe from this group and stop receiving emails from it, send an >email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

> Actually, you don't need strict equality on categories to talk about > strict Grothendieck fibrations in type theory: > https://ncatlab.org/nlab/show/displayed+category This is indexed and not fibered (see my MR review of this paper). Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

It may be "indexed" in the sense that it involves maps into a universe, but it is not an "indexed category" as the term is usually used, since the latter is a pseudofunctor into Cat rather than a lax functor into Span. In particular, a displayed category can be a fibration, an opfibration, both, or neither, while an indexed category always corresponds to at least a fibration. A displayed category is a refinement of a functor in the same way that a dependent type is a refinement of a function: you can always recover the total category by taking Sigma-types, and thereby formulate all of the theorems mentioned in your MR review. The advantage of "presenting" a functor as a displayed category is that it solves precisely the problem at issue, giving a way of talking about two objects being "in the same (strict) fiber" without invoking equality of objects in the base category. Requiring the type of objects of a category to be an h-set does also recover the ability to talk about strict fibers, but the resulting theory of "Grothendieck fibrations" would be pretty useless for HoTT, since almost no naturally-occurring categories have this property or can even be replaced by equivalent categories that have this property. If we want a theory of categories that includes important things like the category of sets, and toposes and geometric morphisms constructed from it, we cannot require all categories to have h-sets of objects (i.e. to be "strict categories"). Thus, to talk about fibrations, we have to either use something like displayed categories, or a weaker notion of fibration such as mentioned by Emily (in which case one simply talks about "essential fibers" rather than strict fibers, and these do have reindexing functors and all the other behavior one would expect). On Thu, Nov 8, 2018 at 1:08 PM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > > Actually, you don't need strict equality on categories to talk about > > strict Grothendieck fibrations in type theory: > > https://ncatlab.org/nlab/show/displayed+category > > This is indexed and not fibered (see my MR review of this paper). > > Thomas > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1200 bytes --] On Wednesday, 7 November 2018 10:03:17 UTC, Ali Caglayan wrote: > > I want to get a general idea of peoples opinions when it comes to naming > categories internal to HoTT. > > On the one hand I have seen, in the HoTT book for example, precategory and > category being used where the latter has the map idtoiso being an > equivalence. > > On the other hand I have seen people call these categories and univalent > categories which is also fine. > > Now because we have Rezk completion every precategory is yearning to > become a category, so some might argue that a distinction isn't necessery. > I would argue that the HoTT book convention is infact more misleading as > "precategory" there is really just the usual notion of category. And a > univalent category is some nice structure we can add to it because we are > working in HoTT. > > What are your thoughts and opinions on this? > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1615 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 5420 bytes --] We have two separate issues here: (1) What is the appropriate notion of category for univalent mathematics. (2) What is the right terminology for it. There is also a separate, orthogonal question, (3) Whether there is a foundation-independent (dubbed "agnostic") notion of category, which gives the right notion for each foundation, *and* can be formulated in MLTT (without K or univalence). Regarding (3), even if this is possible (assuming the question makes sense), it is not given by any of the proposed notions, and this should not be regarded as surprising or shocking. (This raises the question of whether there is a categorical definition of category, for people who would like to see category theory itself as a foundation.) Regarding (1), I think the arguments by Ulrik, Paolo, Mike and Eric (Finster) are pretty convincing: "univalent category" is the right notion of category for univalent mathematics. However, it *is* common and useful in mathematics to formulate and prove theorems with minimal hypotheses, and then what is called a pre-category, and what Thorsten called a wild category, often arise naturally and unavoidably as part of the building blocks of mathematics. Regarding (2), I would say, in view of (the answer to) (3), that it is probably better to avoid the naked terminology "category" in HoTT/UF, as it would give the wrong impression of *capturing* a universal, pre-existing, foundation-independent notion of category (in particular compatible with the ZFC view of what a category is, which has evilness as a built-in feature): * Then "univalent category" could mean, ambiguously but consistently, both (a) a pre-category that satisfies a certain technical condition analogous to the univalence axiom for types, or (b) "the appropriate notion of category for univalent mathematics". (c) In both cases, (a) and (b), the adjective "univalent" makes sense. In (b), it would be not in opposition to "category", but instead in opposition to e.g. "ZFC category". Martin On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote: > > I strongly agree with Ulrik. Perhaps the point that's not getting > across is that we are not talking about terminology for MLTT in > general, but specifically for HoTT (with univalence). The terminology > to be decided on doesn't have to make sense or come out to anything > meaningful in type theory with UIP, and we shouldn't expect it to. > The terminology in MLTT+UIP should be different from that for MLTT+UA, > because they are different theories and relate to "traditional" > mathematics in different *incompatible* ways. I doubt there is *any* > choice of terminology for plain MLTT without UA *or* UIP that is > sensible in that it can be specialized to the right terminology upon > the addition of either of these two inconsistent axioms. > On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine > <p.l.lu...@gmail.com <javascript:>> wrote: > > > > On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com > <javascript:>> wrote: > >> > >> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch > wrote: > >>> > >>> As I tried to say, I find that precategory is the novel concept, and > that both strict category and univalent category should be familiar to > category theorists. (They have a mental model for when one notion is called > for or the other, but we can make the distinction formal.) > >>> > >>> > >>> This is too clever! > >>> > >>> > >>> > >>> If you just transcribe the traditional definition of a category in > type theory you end up with what in the HoTT book is called precategory. > This is confusing for the non-expert even though you can justify why it > should be so. > >> > >> > >> No, you get the notion of a strict category, which in some sense is all > that you directly have in set theory. > > > > > > No in turn: you can arguably get either strict categories, or > precategories, or what Thorsten dubbed “wild categories” above, since “set” > in set theory is the (naïve) interpretation of both “set” and “type”. > (Just as when you transcribe classical definitions in a constructive > setting, you sometimes want to read “predicate” just as “predicate” and > other times as “decidable predicate” — all predicates are decidable > classically, but that doesn’t mean that their constructive transcription > should include “decidable” by default.) > > > > –p. > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. > > > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 7439 bytes --]

If one wants a name for "pre-category" that sounds less derogatory, one could say "flagged category". Talking about "flagged categories", "strict categories", and "univalent categories" will always be unambiguous, and individual papers could declare that plain "category" will locally mean one or another as desired. On Thu, Nov 8, 2018 at 1:37 PM Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > We have two separate issues here: > > (1) What is the appropriate notion of category for univalent > mathematics. > > (2) What is the right terminology for it. > > There is also a separate, orthogonal question, > > (3) Whether there is a foundation-independent (dubbed "agnostic") > notion of category, which gives the right notion for each > foundation, *and* can be formulated in MLTT (without K or > univalence). > > Regarding (3), even if this is possible (assuming the question > makes sense), it is not given by any of the proposed notions, and > this should not be regarded as surprising or shocking. > > (This raises the question of whether there is a categorical > definition of category, for people who would like to see category > theory itself as a foundation.) > > Regarding (1), I think the arguments by Ulrik, Paolo, Mike and > Eric (Finster) are pretty convincing: "univalent category" is the > right notion of category for univalent mathematics. > > However, it *is* common and useful in mathematics to formulate > and prove theorems with minimal hypotheses, and then what is > called a pre-category, and what Thorsten called a wild category, > often arise naturally and unavoidably as part of the building > blocks of mathematics. > > Regarding (2), I would say, in view of (the answer to) (3), that > it is probably better to avoid the naked terminology "category" > in HoTT/UF, as it would give the wrong impression of *capturing* > a universal, pre-existing, foundation-independent notion of > category (in particular compatible with the ZFC view of what a > category is, which has evilness as a built-in feature): > > * Then "univalent category" could mean, ambiguously but > consistently, both > > (a) a pre-category that satisfies a certain technical > condition analogous to the univalence axiom for > types, or > > (b) "the appropriate notion of category for univalent > mathematics". > > (c) In both cases, (a) and (b), the > adjective "univalent" makes sense. In (b), it > would be not in opposition to "category", but > instead in opposition to e.g. "ZFC category". > > Martin > > > On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote: >> >> I strongly agree with Ulrik. Perhaps the point that's not getting >> across is that we are not talking about terminology for MLTT in >> general, but specifically for HoTT (with univalence). The terminology >> to be decided on doesn't have to make sense or come out to anything >> meaningful in type theory with UIP, and we shouldn't expect it to. >> The terminology in MLTT+UIP should be different from that for MLTT+UA, >> because they are different theories and relate to "traditional" >> mathematics in different *incompatible* ways. I doubt there is *any* >> choice of terminology for plain MLTT without UA *or* UIP that is >> sensible in that it can be specialized to the right terminology upon >> the addition of either of these two inconsistent axioms. >> On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine >> <p.l.lu...@gmail.com> wrote: >> > >> > On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote: >> >> >> >> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote: >> >>> >> >>> As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.) >> >>> >> >>> >> >>> This is too clever! >> >>> >> >>> >> >>> >> >>> If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so. >> >> >> >> >> >> No, you get the notion of a strict category, which in some sense is all that you directly have in set theory. >> > >> > >> > No in turn: you can arguably get either strict categories, or precategories, or what Thorsten dubbed “wild categories” above, since “set” in set theory is the (naïve) interpretation of both “set” and “type”. (Just as when you transcribe classical definitions in a constructive setting, you sometimes want to read “predicate” just as “predicate” and other times as “decidable predicate” — all predicates are decidable classically, but that doesn’t mean that their constructive transcription should include “decidable” by default.) >> > >> > –p. >> > >> > -- >> > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1530 bytes --] The intuitive notion of a category is given by the dependently-sorted algebraic theory of categories. In the ZFC metatheory, a standard model of this theory yields the usual mathematical concept of a category. In the MLTT metatheory, a standard model of this theory yields the concept of a precategory. The subtle issue is how to treat the equality predicate, appearing in the identity and associativity axioms. In set theory, equality is a former of atomic formulae, which are a different syntactic category than sets (which interpret the types/domains of the given language). In type theory, equality is interpreted as any other type, in accordance with "the formulae-as-types notion of construction". However, more modern type theories, like HoTT or CubicalTT, have a different, "native" conception of equality, so the "natural" notion of category in these theories will accordingly be different as well. One day, there might be a metatheory which is generally accepted as providing a superior "natural" notion of a category, that avoids the awkward points of the set-theoretic one. Until then, it is best to be precise with language, always being explicit which specific concept is meant. Cheers, Andrew -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1990 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1302 bytes --] On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote: > > The intuitive notion of a category is given by the dependently-sorted > algebraic theory of categories. > Maybe for you! But not for me: I don't even know what a dependently-sorted algebraic theory is, where and how such a thing has models, nor what the particular theory you're thinking of is. But that reminds me of a MATHEMATICAL question. Consider the well-known essentially algebraic theory T whose models in Set are strict categories. What are the models of T in infinity-groupoids? (Or in an arbitrary (infinity,1)-topos?) > However, more modern type theories, like HoTT or CubicalTT, have a > different, "native" conception of equality, so the "natural" notion of > category in these theories will accordingly be different as well. > In cubical type theories, the two notions of equality (path types and the inductive Id-family) are equivalent, so they give equivalent notions wherever they are used. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1896 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2210 bytes --] On Fri, 9 Nov 2018, at 10:18 AM, Ulrik Buchholtz wrote: > On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote: > > > > The intuitive notion of a category is given by the dependently-sorted > > algebraic theory of categories. > > > > Maybe for you! But not for me: I don't even know what a dependently-sorted > algebraic theory is, where and how such a thing has models, nor what the > particular theory you're thinking of is. Let's say we define a *dependently-sorted algebraic theory* to just be a CwF. A model for it is a CwF-morphism into Set (or more generally into a CwF). The theory of categories would then be the opposite of Cat_{fp} (I mean finitely presentable, *not* locally finitely presentable), or alternatively you can define it inductively as the syntax of a type theory (but then you have to prove an initiality theorem!). I'm not sure how this kind of presentation translates to ∞-categories though. > But that reminds me of a MATHEMATICAL question. Consider the well-known > essentially algebraic theory T whose models in Set are strict categories. > What are the models of T in infinity-groupoids? (Or in an arbitrary > (infinity,1)-topos?) Nice question! I guess by model here you mean a left exact ∞-functor T → Space, where T is regarded as an ordinary category with finite limits. I think such models are equivalent to Segal spaces, but without completeness. Or at least, I don't see where completeness would come from. I find it quite an illuminating way to look at Segal spaces, by the way. You get the space of n-simplices by mapping the iterated pullback of the object of arrows in T (i.e. the object that stands for sequences of composable arrows). The Segal condition is the preservation of that pullback. It's essentially the same idea as in the definition of Γ-Spaces. Best, Paolo -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2766 bytes --]

Benedikt and Peter essentially employ an old result of Benabou saying that functors to BB correspond normalized lax functor from BB^op to Dist, the bicategory of distributors. But, obviously, the forward direction requires equality of objects. Accordingly, they can't express composition of functors in terms of the associated normalized lax functors. Even classically, going from fibrations to indexed categories involves choice. But going from functors to normalized lax functors just requires equality of objects. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Right, the *forward* direction requires either equality of objects or using "essential fibers" instead of fibers. That's what I meant by saying a displayed category is a "refinement" of a functor: you can make a functor from a displayed category, but the opposite direction is harder. That doesn't mean that you can't express composition of functors in terms of displayed categories: it just means you can't (or shouldn't) do it in the naive way by first making your displayed categories into functors, composing them, and then going back to a displayed category. Instead you just have to "lift" functor composition to displayed categories in the same way that we lift function composition to Sigma-types. Suppose D is a displayed category over C, with types of objects obD(x) : Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C) and f:hom_C(x,y). Then we can form a total category Sigma(C)D whose type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms are similar Sigma-types. Now suppose we have a further displayed category E over Sigma(C)D. Then applying associativity of Sigma-types, we can construct a displayed category Sigma(D)E over C, with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so on, whose total category is equivalent (indeed, definitionally isomorphic, if Sigma-types have definitional beta and eta) to Sigma(Sigma(C)D)E such that its projection functor corresponds to the composite of the two functors. On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > Benedikt and Peter essentially employ an old result of Benabou saying that > functors to BB correspond normalized lax functor from BB^op to Dist, > the bicategory of distributors. But, obviously, the forward direction requires > equality of objects. > Accordingly, they can't express composition of functors in terms of > the associated normalized lax functors. > > Even classically, going from fibrations to indexed categories involves > choice. But going from functors to normalized lax functors just > requires equality of objects. > > Thomas > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Didn't deny that it's possible in principle for this very simple case. But something trivial gets unnaturally complicated when changing foundations. That's already showing that the new foundation is not superior in all aspects but actually much worse in particular cases. This is not unexpected anway that different formalisms have different advantages and drawbacks. The interesting thing would be to find out what is easier and what is more cumbersome in which framework. As I said in a previous mail. Traditional approaches didn't have universes and fibrations were partly invented to overcome this shortcoming at the price of having to externalize reasoning. But there is also extensional type theory with universes. Maybe that's better than the other 2 approaches. But one cannot say beforehand which setting is better for what. What experience tells us is that different setting are good/bad for different purposes. That's the point I wanted to make. From my side no need for further discussion... Thomas > Right, the *forward* direction requires either equality of objects or > using "essential fibers" instead of fibers. That's what I meant by > saying a displayed category is a "refinement" of a functor: you can > make a functor from a displayed category, but the opposite direction > is harder. That doesn't mean that you can't express composition of > functors in terms of displayed categories: it just means you can't (or > shouldn't) do it in the naive way by first making your displayed > categories into functors, composing them, and then going back to a > displayed category. Instead you just have to "lift" functor > composition to displayed categories in the same way that we lift > function composition to Sigma-types. > > Suppose D is a displayed category over C, with types of objects obD(x) > : Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C) > and f:hom_C(x,y). Then we can form a total category Sigma(C)D whose > type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms > are similar Sigma-types. Now suppose we have a further displayed > category E over Sigma(C)D. Then applying associativity of > Sigma-types, we can construct a displayed category Sigma(D)E over C, > with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so > on, whose total category is equivalent (indeed, definitionally > isomorphic, if Sigma-types have definitional beta and eta) to > Sigma(Sigma(C)D)E such that its projection functor corresponds to the > composite of the two functors. > On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher > <streicher@mathematik.tu-darmstadt.de> wrote: -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.