Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 12th 2010
   • PermaLink
   Author: Urs
   Format: MarkdownI split off [[inhabited object]] from [[inhabited set]]. (moved Mike's and Toby's old discussion query box to the new entry, too) I added an Examples section with a remark about this issue in the context of [[Models for Smooth Infinitesimal Analysis]], that I happen to be looking into. personally, I feel I need more examples still at [[internal logic]] to follow this in its full scope. I guess I should read the Elephant one day, finally. In the book Moerdijk-Reyes say in a somewhat pedestrian way that existential quantifiers in the internal logic of a sheaf topos are to be evaluated on covers, hence asking internally if a sheaf <latex>F</latex> has a (internally global) element means asking if for <latex> U \to * </latex> any cover of the point, there is a morphism <latex> U \to F</latex>. That's fine with me and I follow this in as far as the purpose of their book is concerned, but I need to get a better idea of how the logical quantifiers are formulate in internal logic in full generality.

   I split off inhabited object from inhabited set.

   (moved Mike's and Toby's old discussion query box to the new entry, too)

   I added an Examples section with a remark about this issue in the context of Models for Smooth Infinitesimal Analysis, that I happen to be looking into.

   personally, I feel I need more examples still at internal logic to follow this in its full scope. I guess I should read the Elephant one day, finally.

   In the book Moerdijk-Reyes say in a somewhat pedestrian way that existential quantifiers in the internal logic of a sheaf topos are to be evaluated on covers, hence asking internally if a sheaf has a (internally global) element means asking if for any cover of the point, there is a morphism .

   That's fine with me and I follow this in as far as the purpose of their book is concerned, but I need to get a better idea of how the logical quantifiers are formulate in internal logic in full generality.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 12th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownI tried to clarify and incorporate the outcome of the old discussion box. I find the "Kripke-Joyal semantics" to be the most edifying way to think about the meaning of the internal logic in terms of the external properties of the category. (It's also the way to generalize the internal logic to the "stack semantics" for unbounded quantifiers.) Kripke-Joyal semantics isn't in the Elephant for some reason, but it's in [[Sheaves in Geometry and Logic]].

   I tried to clarify and incorporate the outcome of the old discussion box.

   I find the "Kripke-Joyal semantics" to be the most edifying way to think about the meaning of the internal logic in terms of the external properties of the category. (It's also the way to generalize the internal logic to the "stack semantics" for unbounded quantifiers.) Kripke-Joyal semantics isn't in the Elephant for some reason, but it's in Sheaves in Geometry and Logic.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 12th 2010
   • PermaLink
   Author: Urs
   Format: Markdown<blockquote> I find the "Kripke-Joyal semantics" to be the most edifying way to think about the meaning of the internal logic in terms of the external properties of the category. </blockquote> Ah, thanks for the hint, I'll look at that.

   This comment is invalid XHTML+MathML+SVG; displaying source. <div> <blockquote> I find the "Kripke-Joyal semantics" to be the most edifying way to think about the meaning of the internal logic in terms of the external properties of the category. </blockquote> <p>Ah, thanks for the hint, I'll look at that.</p> </div>
4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeOct 11th 2020
   • PermaLink
   Author: Urs
   Format: MarkdownItexThe following old discussion/query box was still sitting in the entry _[[inhabited object]]_. I am hereby moving it from there to here: *** While writing this page, we had the following discussion about whether or not "$X$ is inhabited" in a topos should be interpreted internally or externally, before deciding that we should mention both. +--{.query} _[[Mike Shulman|Mike]]_: I strongly disagree that "inhabited" means "has a global element" in a topos. Intuitionistically, "$X$ is inhabited" means "there exists an $x\in X$" which when interpreted in the internal logic of a topos means that $X$ is well-supported. By contrast, the property of having a global element is not expressible in the internal language at all. "Inhabited" is also universally used in the topos-theoretic literature to mean well-supported. _Toby_: Then what is the term for what I have called 'inhabited'? [At least one reference](http://www.dcs.kcl.ac.uk/technical-reports/papers/tr97-04.ps.gz) uses the term that way; I see (through Google) that it\'s used in the Elephant, but it\'s not in the index and I haven\'t managed to tell what the definition is. Certainly I\'m not in the position to make a good literature search. _Mike_: On p618 of the Elephant he uses "inhabited" to mean "there exists an $x\in X$" in the internal language. What do you think about the change I made above? _Toby_: I certainly can\'t disagree with any of the statements there. I would like us to be a bit bolder with the terminology if it\'s safe and useful (neither of which condition has been established, of course). The Elephant has its share of terminological changes (like 'cartesian category' and 'cartesian morphism', which I remember got a lot of complaints on the categories mailing list), so I\'d want to check its references (which I can do later). The wiki saved a previous version of your comments; since you changed it, I won\'t hold you to it. But having read it does inspire me to say that the terminology that comes naturally to me is indeed 'inhabited' for having a global element and 'internally inhabited' for being well supported; the latter seems at least as well justified as 'internal axiom of choice' (as used in, say, Mac Lane \& Moerdijk). That\'s just me, of course. _Mike_: Yeah, I wasn't sure if it would (there seems to be a certain timeout within which multiple edits by the same person overwrite each other?). I also wasn't sure if it was kosher to remove/change my comment; perhaps I shouldn't have. The reason I changed it was that "inhabited" and "internally inhabited" did start to make a little sense. My current feeling is that "inhabited" is a set-theoretic term, and as such should only be used in set-theoretic-like situations. This includes (1) constructive set theory, (2) IHOL and hence the internal language of a topos, and (3) a well-pointed topos. If we are talking about an arbitrary topos, and it is not clear that our statements are to be interpreted in the internal logic, I would rather use "has a global element" and "is well-supported" since they are both unambiguous. You are certainly right about the Elephant and terminology. "Cartesian category," "prone morphism," and "effective regular category" are the ones that come to mind that seem to have been rejected by much of the categorical community. _Mike_: Another thought: one could argue that just as a "ring" in a topos means a model of the theory of rings, and likewise for many other concepts, so should an "inhabited object" mean a model of the theory of inhabited objects, which is the same as a well-supported object. Of course this fails for "projective object," but I don't think there is a "theory of projective objects," at least not one interpetable in the usual internal logic of a topos. And I suppose maybe it fails for "choice object" too, although that probably depends on whether you formulate the theory of choice objects to be equipped with a choice function or merely assert that one exists. Perhaps the literature is not very consistent in its use of "internally" or lack thereof. _Toby_: I see 'inhabited' as just a convenient abbreviation of 'that has an element' (convenient enough that 'is inhabited' is still nicer than 'has an element'). So an inhabited object should naturally be an object with an element (a global element, that is; every object has a generalised element, and we must at least reproduce the situation in $\Set$). And after all, 'inhabited' is hardly more of a set-theoretic term than 'axiom of choice'! (^_^) Maybe life would be simpler if we always internalised using the internal language, but there\'s a lot of precedent that we don\'t, probably because it\'s a lot easier not to. And anyway, that\'s what the word 'internalised' is for! As for the timeout, I think that it\'s an hour, although I haven\'t timed it carefully. (It definitely exists.) I think that it\'s fine to remove or change old comments, certainly if they haven\'t been replied to, but one should be aware that they can still be read. (And if you\'re not sure if they can still be read, try 'See changes' or 'Back in time' below.) _Mike_: Well, I think that I will continue using "has a global element" myself for clarity, but you've convinced me that it's not entirely unreasonable to use "is inhabited" to mean the same thing. Though I reserve the right to reopen the discussion if we discover precendent to the contrary. (-: A different question, as you mentioned earlier, is whether it is useful. How often do we want to talk about objects that have a global element? We may frequently care about _pointed_ objects, which are _equipped_ with a global element, but there isn't any dispute about what to call those. _Toby_: You\'ve got a good point there. Probably 'pointed object' and 'well-supported object' are the only really useful notions. Actually, I think that a lot of constructivists (the ones that are really think that mathematics should talk about *constructions*, like Bishop and Coquand) would say that an inhabited set and a pointed set are really the same thing. We can distinguish them, of course, by their morphisms (or even isomorphisms), but that doesn\'t mean that we need two words (just as we don\'t use two different words for metric spaces with, say, continuous maps between them and uniformly continuous maps bewteen them). So as you move towards my position, I move towards yours .... _Mike_: Does that mean you might be satisfied with the way it's written now? (I added a note about pointed objects.) _Toby_: Yes, I\'m happy now for now. =-- *** <a href="https://ncatlab.org/nlab/revision/diff/inhabited+object/9">diff</a>, <a href="https://ncatlab.org/nlab/revision/inhabited+object/9">v9</a>, <a href="https://ncatlab.org/nlab/show/inhabited+object">current</a>

   The following old discussion/query box was still sitting in the entry inhabited object. I am hereby moving it from there to here:

   ---

   While writing this page, we had the following discussion about whether or not “$X$ is inhabited” in a topos should be interpreted internally or externally, before deciding that we should mention both.

   +–{.query}

   Mike: I strongly disagree that “inhabited” means “has a global element” in a topos. Intuitionistically, “$X$ is inhabited” means “there exists an $x\in X$” which when interpreted in the internal logic of a topos means that $X$ is well-supported. By contrast, the property of having a global element is not expressible in the internal language at all. “Inhabited” is also universally used in the topos-theoretic literature to mean well-supported.

   Toby: Then what is the term for what I have called ’inhabited’? At least one reference uses the term that way; I see (through Google) that it's used in the Elephant, but it's not in the index and I haven't managed to tell what the definition is. Certainly I'm not in the position to make a good literature search.

   Mike: On p618 of the Elephant he uses “inhabited” to mean “there exists an $x\in X$” in the internal language. What do you think about the change I made above?

   Toby: I certainly can't disagree with any of the statements there.

   I would like us to be a bit bolder with the terminology if it's safe and useful (neither of which condition has been established, of course). The Elephant has its share of terminological changes (like ’cartesian category’ and ’cartesian morphism’, which I remember got a lot of complaints on the categories mailing list), so I'd want to check its references (which I can do later).

   The wiki saved a previous version of your comments; since you changed it, I won't hold you to it. But having read it does inspire me to say that the terminology that comes naturally to me is indeed ’inhabited’ for having a global element and ’internally inhabited’ for being well supported; the latter seems at least as well justified as ’internal axiom of choice’ (as used in, say, Mac Lane \& Moerdijk). That's just me, of course.

   Mike: Yeah, I wasn’t sure if it would (there seems to be a certain timeout within which multiple edits by the same person overwrite each other?). I also wasn’t sure if it was kosher to remove/change my comment; perhaps I shouldn’t have. The reason I changed it was that “inhabited” and “internally inhabited” did start to make a little sense. My current feeling is that “inhabited” is a set-theoretic term, and as such should only be used in set-theoretic-like situations. This includes (1) constructive set theory, (2) IHOL and hence the internal language of a topos, and (3) a well-pointed topos. If we are talking about an arbitrary topos, and it is not clear that our statements are to be interpreted in the internal logic, I would rather use “has a global element” and “is well-supported” since they are both unambiguous.

   You are certainly right about the Elephant and terminology. “Cartesian category,” “prone morphism,” and “effective regular category” are the ones that come to mind that seem to have been rejected by much of the categorical community.

   Mike: Another thought: one could argue that just as a “ring” in a topos means a model of the theory of rings, and likewise for many other concepts, so should an “inhabited object” mean a model of the theory of inhabited objects, which is the same as a well-supported object. Of course this fails for “projective object,” but I don’t think there is a “theory of projective objects,” at least not one interpetable in the usual internal logic of a topos. And I suppose maybe it fails for “choice object” too, although that probably depends on whether you formulate the theory of choice objects to be equipped with a choice function or merely assert that one exists. Perhaps the literature is not very consistent in its use of “internally” or lack thereof.

   Toby: I see ’inhabited’ as just a convenient abbreviation of ’that has an element’ (convenient enough that ’is inhabited’ is still nicer than ’has an element’). So an inhabited object should naturally be an object with an element (a global element, that is; every object has a generalised element, and we must at least reproduce the situation in $\Set$). And after all, ’inhabited’ is hardly more of a set-theoretic term than ’axiom of choice’! (^_^)

   Maybe life would be simpler if we always internalised using the internal language, but there's a lot of precedent that we don't, probably because it's a lot easier not to. And anyway, that's what the word ’internalised’ is for!

   As for the timeout, I think that it's an hour, although I haven't timed it carefully. (It definitely exists.) I think that it's fine to remove or change old comments, certainly if they haven't been replied to, but one should be aware that they can still be read. (And if you're not sure if they can still be read, try ’See changes’ or ’Back in time’ below.)

   Mike: Well, I think that I will continue using “has a global element” myself for clarity, but you’ve convinced me that it’s not entirely unreasonable to use “is inhabited” to mean the same thing. Though I reserve the right to reopen the discussion if we discover precendent to the contrary. (-:

   A different question, as you mentioned earlier, is whether it is useful. How often do we want to talk about objects that have a global element? We may frequently care about pointed objects, which are equipped with a global element, but there isn’t any dispute about what to call those.

   Toby: You've got a good point there. Probably ’pointed object’ and ’well-supported object’ are the only really useful notions. Actually, I think that a lot of constructivists (the ones that are really think that mathematics should talk about constructions, like Bishop and Coquand) would say that an inhabited set and a pointed set are really the same thing. We can distinguish them, of course, by their morphisms (or even isomorphisms), but that doesn't mean that we need two words (just as we don't use two different words for metric spaces with, say, continuous maps between them and uniformly continuous maps bewteen them). So as you move towards my position, I move towards yours ….

   Mike: Does that mean you might be satisfied with the way it’s written now? (I added a note about pointed objects.)

   Toby: Yes, I'm happy now for now.

   =–

   ---

   diff, v9, current