\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*{stack semantics}

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

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{stack_semantics}{}\section*{{Stack semantics}}\label{stack_semantics}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{direct_description}{Direct description}\dotfill \pageref*{direct_description} \linebreak
\noindent\hyperlink{as_internal_logic}{As internal logic}\dotfill \pageref*{as_internal_logic} \linebreak
\noindent\hyperlink{relationship_to_locally_internal_categories}{Relationship to locally internal categories}\dotfill \pageref*{relationship_to_locally_internal_categories} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

The \textbf{stack semantics} is an extension of the [[internal logic]] of a [[category]] (or [[higher category]]) $C$ which allows us to talk about, and [[quantifier|quantify over]], \emph{objects} of $C$. (Such quantification is sometimes called ``unbounded'' quantification.)

In the ordinary internal language, an internal ``element'' of an object $A$ is interpreted into a [[generalized element]] $X\to A$ for some object $X\in C$, which consists intuitively of one ``actual'' element of $A$ for every element of $X$. Similarly, in the stack semantics, an internal ``object'' is interpreted as a ``generalized object'' defined at some stage $X$, which we define to mean an object of the [[slice category]] $C/X$. This makes sense because an object of $C/X$ consists intuitively of one ``actual'' object of $C$ for each ``element'' of $X$ (namely, the [[fiber]] over that element).

The stack semantics is so-called because in most categories $C$ where we consider it (such as [[toposes]] or [[pretoposes]]), the [[self-indexing]] is a [[stack]] for some naturally defined [[Grothendieck topology]] on $C$, and the stack semantics can be regarded as the ordinary internal logic of a higher topos of stacks on $C$ (see below). Analogously, the ordinary internal logic is often called \emph{sheaf semantics}, because in a [[subcanonical topology]] all [[representable functors]] are [[sheaves]], and because it can often be regarded as part of the internal logic of the topos of sheaves on $C$.

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

\hypertarget{direct_description}{}\subsubsection*{{Direct description}}\label{direct_description}

\ldots{}

\hypertarget{as_internal_logic}{}\subsubsection*{{As internal logic}}\label{as_internal_logic}

While on the one hand, the stack semantics \emph{generalizes} the internal logic of a category, it can also be regarded as a special case thereof.

The basic idea of this is that if we have a chosen morphism $\widetilde{U}\to U$ in $C$, then generalized elements of $U$ at stage $X$ can be regarded as ``names'' for generalized \emph{objects} of $C$ at stage $X$. Namely, the generalized element $u\colon X\to U$ names the [[pullback]] of $\widetilde{U}\to U$ along $u$.

There are two issues with this idea, which can prevent it from faithfully representing the \emph{idea} of the stack semantics sketched above.

The first issue is that a given ``generalized object'' over $X$ may have multiple names, whereas the stack semantics ought to speak directly about objects rather than about names for them. Moreover, since $C/X$ is actually a category (or a higher category, if $C$ is such), generalized objects [[evil|should]] be considered ``the same'' only if they are [[isomorphism|isomorphic]] or [[equivalence|equivalent]], whereas morphisms $X\to U$ may admit a stricter notion of sameness. In particular, when $C$ is a [[1-category]] (the classical case), the morphisms $X\to U$ form a \emph{set}, whereas $C/X$ should be regarded as a category, or at worst as a [[groupoid]] (its [[core]]).

More generally, if $C$ is an [[n-category]] for some finite $n$, then $C(X,U)$ is only an $(n-1)$-category, whereas $C/X$ is also an $n$-category or at worst an [[n-groupoid]]. Thus, there is no hope of solving this problem \emph{inside} of $C$ unless $C$ is at least an [[(∞,1)-category]]. In that case, the notion of [[object classifier in an (∞,1)-category]] does solve this problem: the $\infty$-groupoid $C(X,U)$ is equivalent to the core of (a suitable subcategory of) $C/X$. (The presence of noninvertible morphisms in $C/X$ is not nearly so big a problem; at least when $C$ is an $(n,1)$-category, these can be described already in the ordinary internal logic if $C$ is [[locally cartesian closed category]].)

If $C$ is only an $(n,1)$-category for some finite $n$, however, then in order to obtain its stack semantics as an internal logic, we must pass to some higher category containing it which is at least an $(n+1,1)$-category. The obvious choice is a category of [[presheaves]] or [[sheaves]]/[[stacks]] on $C$ valued in $n$-categories or $n$-groupoids (or $m$-groupoids for some $m\ge n$).

The second issue is that not every ``generalized object'' over $X$ may have a name. This is almost impossible to get around while remaining within $C$, due to issues with paradoxes. Even [[object classifiers in an (∞,1)-category]] only classify the core of some [[subcategory]] of $C/X$.

One way to deal with this is to suppose some (possibly [[ordinal|transfinite]]) sequence of object classifiers, each contained in the next, such that every generalized object is eventually classified by some one of them. In the internal logic, this corresponds roughly to the idea of [[universe polymorphism]] in [[type theory]].

Another way is, of course, to move outside of $C$. In particular, if we work in a category of presheaves/sheaves/stacks on $C$ at one category-level up, then the [[self-indexing]] of $C$ (or its [[core]]) will be an object $U$ which classifies \emph{exactly} the desired category $C/X$ of generalized objects for each $X\in C$. (The exhaustive sequence of universes can also be regarded as moving outside of $C$, perhaps to a category of [[ind-objects]] in $C$.) The fragment of the internal logic of this category of stacks which deals only with objects of $C$ itself can then be identified with the direct Kripke-Joyal style stack-semantics described above.

Of course, one can also embrace this second limitation and just live with a ``partial'' stack semantics that only allows us to talk about a particular subclass of generalized objects. The [[Mitchell-Bénabou language]] of a [[topos]] can be regarded as a partial stack semantics in this sense, in which the only generalized objects we can classify over are the [[subterminal objects]] (i.e. the [[subobjects]] $A \hookrightarrow X$). The object $U$ in this case is, of course, the [[subobject classifier]].

One can also embrace the first limitation and not worry about having multiple names for the same object. This leads to notions such as a [[universe in a topos]] and the field of [[algebraic set theory]].

\hypertarget{relationship_to_locally_internal_categories}{}\subsection*{{Relationship to locally internal categories}}\label{relationship_to_locally_internal_categories}

The stack semantics for a topos $\mathcal{E}$ can be used to talk about [[locally internal category|locally internal categories]] of $\mathcal{E}$ (in the sense of (\hyperlink{Penon}{Penon 1974})) as if they're ordinary locally small categories over $\mathrm{Set}$.

Examples:

\begin{itemize}%
\item A geometric morphism $f: \mathcal{F} \to \mathcal{E}$ looks like the canonical morphism $\mathcal{F} \to \mathrm{Set}$ when using the stack semantics of $\mathcal{E}$.


\item The internal statement ``$\mathcal{F}$ is a compact topos'' is equivalent to $f$ being a [[proper geometric morphism|proper morphism]].


\item The internal statement ``$\mathcal{F}$ is an indiscrete topos'' (i.e. ``the canonical morphism $\mathrm{Sub}_{\mathcal{F}}(1) \to \mathrm{Sub}_{\mathrm{Set}}(1)$ is a bijection'', where $\mathrm{Sub}$ refers to the corresponding [[poset of subobjects|posets of subobjects]]) is true iff $f$ is [[hyperconnected geometric morphism|hyperconnected]].


\item Because the proof that indiscrete toposes are compact is constructive, it immediately follows that hyperconnected morphisms are proper.



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

\begin{itemize}%
\item [[semantics]]


\item [[Kripke-Joyal semantics]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Mike Shulman]], \emph{\href{http://arxiv.org/abs/1004.3802}{Stack semantics and the comparison of material and structural set theories}} (2010)


\item J. Penon, \emph{Categories localement internes}, C. R. Acad. Sci. Paris \textbf{278} (1974) A1577-1580



\end{itemize}
\begin{itemize}%
\item Locally internal categories, Appendix in: [[Peter Johnstone]], \emph{Topos theory}, London Math. Soc. Monographs \textbf{10}, Acad. Press 1977, xxiii+367 pp.

\end{itemize}


\end{document}