\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{inhabited object}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{category_theory}{}\paragraph*{{Category Theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{in_a_wellpointed_topos}{In a well-pointed topos}\dotfill \pageref*{in_a_wellpointed_topos} \linebreak
\noindent\hyperlink{discussion}{Discussion}\dotfill \pageref*{discussion} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In [[category theory]] and specifically in [[topos theory]], the notion of \emph{inhabited object} in a general [[topos]] is a generalization of the notion of [[inhabited set]] from the archetypal topos [[Set]]. It is the [[semantics]] of an [[inhabited type]] in [[type theory]].

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

An object $X$ in a [[topos]] $\mathcal{T}$ is said to be \textbf{internally inhabited} if in the [[internal logic]] of the topos it is true that

\begin{displaymath}
\exists x \in X.
\end{displaymath}
This is equivalent to saying that the unique map $X \to 1$ is an [[epimorphism]]. More generally, we can make the same definition in any [[regular category]], in which case it is equivalent to $X\to 1$ being a [[regular epimorphism]].

The term \textbf{well-supported} is also used for this notion (in general, the [[support]] of $X$ is the [[image]] of $X\to 1$).

In terms of [[(∞,1)-category theory]], internally inhabited means \emph{[[(-1)-connected]]}.

On the other hand, $X$ is said to be \textbf{externally} or \textbf{globally inhabited} if there exists a morphism $1\to X$, i.e. a [[global element]]. The adjective ``externally'' is perhaps misleading, since this notion can also be expressed in the internal [[type theory]] of the topos (as having an [[element]]/[[term]] $x:X$), though not in its more usual internal [[higher-order logic]]. The internal assertion ``every internally inhabited object is globally inhabited'' is a version of the [[propositional axiom of choice]] (PAC).

Every globally inhabited object is internally inhabited, since every [[split epimorphism]] is a regular epimorphism. The converse is true if $1$ is [[projective object|projective]], as is the case in a [[well-pointed topos]] (such as [[Set]]). (This may seem to contradict the above, since PAC can fail even in (constructively) well-pointed toposes, but the point is that PAC also says something about \emph{families} of inhabited objects rather than single ``globally defined'' objects.)

Some sources use ``$X$ is inhabited'' in the global sense, while others use the term ``inhabited'' only internally. Regardless, a [[pointed object]] always means one \emph{equipped with} a global element $1\to X$ (which is the same whether interpreted internally or externally), and the terms ``global element'' and ``well-supported'' are always unambiguous.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

For [[Grothendieck topos|sheaf toposes]] with [[point of a topos|enough points]], in which epimorphisms are [[stalk]]wise epimorphisms, an object is (internally) inhabited if the [[germ]] of $X$ over every [[stalk]] is an [[inhabited set]].

One situation where this plays a role is in the study of certain [[smooth topos]]es with objects $\mathbb{I}$ of \emph{invertible infinitesimals} . There is an immediate definition of such a topos, the topos called $\mathcal{Z}$ at [[Models for Smooth Infinitesimal Analysis]], for which this object exists, but is not inhabited. Only the weaker internal statement $\not \not \exists x \in \mathbb{I}$ is true.

But for some useful constructions in these toposes, such as for giving an internal definition of [[distribution]]s as genuine functions (internally), it is desirable to have $\mathbb{I}$ be inhabited. In the above situation this is achieved by [[forcing]] the existence of invertible infinitesimal elements. The result is the refined topos denoted $\mathcal{B}$ at [[Models for Smooth Infinitesimal Analysis]].

\hypertarget{in_a_wellpointed_topos}{}\subsection*{{In a well-pointed topos}}\label{in_a_wellpointed_topos}

The category [[Set]] is a very special sort of topos. A generally useful principle in formulating categorical properties of [[Set]] is that ``external'' and ``internal'' notions should coincide. A general default understanding across the nLab is that $Set$ is a [[well-pointed topos]] whose terminal object $1$ is projective and [[indecomposable object|indecomposable]]. These latter properties of the terminal object hold for any well-pointed topos if the metalogic is [[classical logic|classical]]; for purposes of [[constructive mathematics]], we usually agree to add them in.

As remarked above, projectivity of $1$ easily makes internal and external inhabitedness agree. We also present a constructive/intuitionistic proof of the following result about \emph{emptiness}.

\begin{prop}
\label{}\hypertarget{}{}
In a well-pointed topos, an object $X$ which is \emph{not} internally inhabited is empty (is an initial object).

\end{prop}
Note that the negation ``not'' in this statement is an \emph{external} one, which is what makes it nontrivial. If an object is \emph{internally} ``not inhabited'', then it is empty essentially by definition.

\begin{proof}
Let $X \to U \hookrightarrow 1$ be the epi-mono factorization of the unique map $X \to 1$. Here $m: U \hookrightarrow 1$ is monic but not epic if $X \to 1$ is not epic, and we use this to prove $U \cong 0$. In that case, we have a map $X \to 0$, whence $X \cong 0$ since in a topos initial objects are strict. (For given $X \to 0$, the projection $\pi_1: X \times 0 \to X$ has a section, and it follows that $X \cong 0$ since $X \times 0 \cong 0$ and retracts of initial objects are initial. This also implies that for any $V$ the map $i: 0 \to V$ is monic: for it is obviously true that for any pair of maps $h, k: A \to 0$ we have that $i h = i k$ implies $h = k$, as $A$ is initial by strictness and this makes $h = k$ automatic.)

Let $f: U \to \Omega$ be the classifying map of the mono $1_U: U \to U$, and let $g: U \to \Omega$ be the classifying map of the mono $0 \to U$. There is no map $1 \to U$, else $m: U \to 1$ would retract it and hence be epic. Hence it is vacuously true that $f x = g x$ for all $x: 1 \to U$, and so $f = g$ by well-pointedness. Hence the subobjects $1_U$ and $0$ coincide, forcing $U \cong 0$. (In other words, the presence of a [[subobject classifier]] causes any [[generator]] to be a [[strong generator]].)

\end{proof}
\hypertarget{discussion}{}\subsection*{{Discussion}}\label{discussion}

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.

\emph{[[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.

\emph{Toby}: Then what is the term for what I have called `inhabited'? \href{http://www.dcs.kcl.ac.uk/technical-reports/papers/tr97-04.ps.gz}{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.

\emph{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?

\emph{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 $\backslash$\& Moerdijk). That's just me, of course.

\emph{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.

\emph{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.

\emph{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'! ({\tt \symbol{94}}\_{\tt \symbol{94}})

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.)

\emph{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 \emph{pointed} objects, which are \emph{equipped} with a global element, but there isn't any dispute about what to call those.

\emph{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 \emph{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 \ldots{}.

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

\emph{Toby}: Yes, I'm happy now for now.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[inhabited set]]

\end{itemize}
[[!redirects well-supported object]] [[!redirects well-supported objects]]

[[!redirects inhabited]]



\end{document}