\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*{elementary (infinity,1)-topos}

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

\hypertarget{category_theory}{}\paragraph*{{$(\infty,1)$-Category theory}}\label{category_theory}

[[!include quasi-category theory contents]]

\hypertarget{topos_theory}{}\paragraph*{{$(\infty,1)$-Topos Theory}}\label{topos_theory}

[[!include (infinity,1)-topos - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition_impredicative_case}{Definition (impredicative case)}\dotfill \pageref*{definition_impredicative_case} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{definition_predicative_case}{Definition (predicative case)}\dotfill \pageref*{definition_predicative_case} \linebreak
\noindent\hyperlink{Examples}{Examples}\dotfill \pageref*{Examples} \linebreak
\noindent\hyperlink{related_pages}{Related pages}\dotfill \pageref*{related_pages} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

The notion of an \emph{elementary (∞,1)-topos} is an analogue of the notion of \emph{[[elementary topos]]} in [[(∞,1)-category theory]]. This is in contrast to the notion of a \emph{Grothendieck} \emph{[[(∞,1)-topos]] [[equivalence of (∞,1)-categories|equivalent]] to an [[(∞,1)-category of (∞,1)-sheaves]]}, the analogue of a [[sheaf topos]], which is more specific (see [[geometric homotopy type theory]]).

Note that every \emph{Grothendieck} [[(∞,1)-topos]] provides [[categorical semantics]] for [[homotopy type theory]] with [[univalence|univalent]] weakly-Tarskian [[types of types]] and also [[higher inductive types]] (HITs). Elementary $(\infty,1)$-toposes ought to be roughly the larger class of \emph{all} $(\infty,1)$-categories that provide [[categorical semantics]] for such homotopy type theory. More precisely, we will define an elementary $(\infty,1)$-topos to have the $(\infty,1)$-categorical structure that ought to correspond to that type-theoretic structure; a [[coherence theorem]] making it \emph{actually} model the corresponding type theory is still unknown.

In general, the problem with ``elementary-izing'' the notion of $(\infty,1)$-topos is that Grothendieck $(\infty,1)$-toposes have many properties that are not reflected in type theory due to the finitary nature of type theory; the question is to find appropriate ``finitary shadows'' of them. For instance, one can construct [[initial algebras for endofunctors]] using a [[transfinite induction]] argument; thus in type theory we postulate the existence of [[inductive types]]. Deciding what class of ``infinitary constructions'' that are available in Grothendieck $(\infty,1)$-toposes can be described finitarily by something that deserves the name ``[[higher inductive type]]'' is overall an open question, but we can obtain reasonable definitions by restricting the class of [[HITs]] we ask for.

\hypertarget{definition_impredicative_case}{}\subsection*{{Definition (impredicative case)}}\label{definition_impredicative_case}

There are at least two ambiguities in the above sketch of a definition based on type theory: what exactly do we assume of the [[universes]] ([[object classifiers]]), and what general class of [[HITs]] do we ask for? One reasonable answer to the universe question is that every object should be contained in a universe closed under all the relevant operations, and one reasonable answer to the HITs question is just the non-recursive ones. This leads to the following definition.

\begin{defn}
\label{}\hypertarget{}{}
An \textbf{elementary $(\infty,1)$-topos} is an $(\infty,1)$-category $\mathbf{E}$ such that

\begin{itemize}%
\item $\mathbf{E}$ has finite [[(∞,1)-limit|limits and colimits]]
\item $\mathbf{E}$ is [[locally cartesian closed (∞,1)-category|locally cartesian closed]]
\item There exists a [[subobject classifier]] (an [[object classifier]] that classifies the collection of all [[monomorphisms in an (∞,1)-category]])
\item For any morphism $f:Y\to X$ in $\mathbf{E}$, there exists an [[object classifier]] in $\mathbf{E}$ classifying a class of morphisms that (1) includes $f$ and (2) is closed under fiberwise finite limits and colimits, composition (i.e. dependent sums), and dependent products.

\end{itemize}
\end{defn}
Note that this definition is ``impredicative'' just like an [[elementary topos]], in that it has a classifier for \emph{all} subobjects. We can't categorify this to a classifier for all objects due to size paradoxes; the existence of ``enough'' object classifiers closed under all the basic operations is the ``next best thing''. We will refer to an object classifier satisfying (2) above as a \textbf{universe}.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

It is reasonable to hope for a coherence theorem showing that any elementary $(\infty,1)$-topos in the above sense admits a model of homotopy type theory with non-recursive [[higher inductive type|HITs]] (corresponding to the the finite colimits), univalent [[type of types|universes]] (perhaps only weakly Tarski ones), and [[propositional resizing]]. See, for instance, \emph{[[homotopytypetheory:model of type theory in an (infinity,1)-topos]]} and \emph{\href{relation+between+type+theory+and+category+theory#HomotopyWithUnivalence}{relation between type theory and category theory -- Univalent homotopy type theory and infinity-toposes}}.

In an elementary 1-topos we can construct finite colimits and dependent exponentials from non-dependent exponentials and the subobject classifier (or equivalently from [[power objects]]). In the $\infty$-case this seems less likely to be true, since subobjects tell us less about objects that are not 0-truncated. However, there is still a good deal of extra structure that ``comes for free'' from the above definition.

\begin{theorem}
\label{}\hypertarget{}{}
The initial object $0$ of $\mathbf{E}$ is [[strict initial object|strict]], i.e. any morphism $A\to 0$ is an equivalence.

\end{theorem}
\begin{proof}
Just as for 1-categories, this is true in any cartesian closed $(\infty,1)$-category. For if there is a morphism $f:A\to 0$ then the projection $A\times 0 \to A$ has a section $(1_A,f)$, so that $A$ is a retract of $A\times 0$; but $A\times 0 \cong 0$ by cartesian closedness since $(A\times -)$ has a right adjoint and hence preserves colimits.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
Binary coproducts in $\mathbf{E}$ are [[disjoint coproducts|disjoint]], i.e. the injections $i:A\to A+B$ and $j:B\to A+B$ are monic, and their pullback is initial.

\end{theorem}
\begin{proof}
This is also just like a corresponding proof for 1-toposes (see [[toposes are extensive]]). Define $R$ and $S$ to make the following squares pullbacks:

\begin{displaymath}
\itexarray{ R & \xrightarrow{r} & A & \xleftarrow{s} & S\\
  ^{r'}\downarrow && \downarrow^i && \downarrow\\
  A & \xrightarrow{i} & A+B & \xleftarrow{j} & B}
\end{displaymath}
Specifically, $(r,r')$ is the [[kernel pair]] of $i$. In particular, there is an induced diagonal $\triangle : A \to R$ such that $r \triangle = 1_A$. On the other hand, since $\mathbf{E}$ is locally cartesian closed, pullback preserves colimits, so $(r,s)$ is a coproduct diagram. Thus, the pair of morphisms $1_R:R\to R$ and $\triangle \circ s : S\to R$ factor (uniquely) through some $h:A\to R$, so that in particular $h r = 1_R$. Thus, $r:R\to A$ has both a left and a right inverse, so it is an equivalence, and hence $i$ is monic. Dually, $j$ is monic.

Now we claim that any two morphisms $f,g:S\to X$ with domain $S$ are equivalent. For the pair of morphisms $R \xrightarrow{r} A \to A+X$ and $S \xrightarrow{f} X \to A+X$ factor uniquely through $A$ (which, recall, is the coproduct $R+S$). But since $r$ is an equivalence, this factorization must be (equivalent to) the left coprojection $A\to A+X$. Therefore, the composite $S \xrightarrow{f} X \to A+X$ is equivalent to the composite $S \xrightarrow{s} A \to A+X$, and similarly so is the composite $S \xrightarrow{g} X \to A+X$. Since $X\to A+X$ is monic by the previous paragraph, $f\simeq g$.

Finally, since $0$ is a strict initial object, $0\to S$ is monic. And of course $1_S : S\to S$ is also monic, and these two monomorphisms are classified by two maps $f,g:S\to \Omega$ into the subobject classifier. By the previous paragraph, $f\simeq g$, hence $S\cong 0$ and is initial.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
For any finite family of morphisms $\{f_i : Y_i \to X_i\}_{i\in I}$, there exists a universe classifying all the $f_i$.

\end{theorem}
\begin{proof}
Since $f_i$ is the pullback of $\sum_i f_i$ along the injection $X_i \to \sum_i X_i$ (this follows from extensivity), a universe classifying $\sum_i f_i$ must also classify each $f_i$.

\end{proof}
In particular, we have ``universe cumulativity'':

\begin{cor}
\label{}\hypertarget{}{}
For any universe $p:V\to U$, there is a universe $p':V'\to U'$ that classifies both $p$ and $U\to 1$.

\end{cor}
\begin{theorem}
\label{}\hypertarget{}{}
All finite colimits are [[van Kampen colimit|van Kampen]].

\end{theorem}
\begin{proof}
Since $\mathcal{E}$ is locally cartesian closed, all colimits are pullback-stable, so it suffices to show descent. Suppose $D$ is a finite [[simplicial set]] and $F^\rhd:G^\rhd:D^\rhd \to \mathcal{E}$ are colimiting cones under diagrams $F,G:D\to \mathcal{E}$, and let $\alpha^\rhd : F\rhd \to G^\rhd$ be a natural transformation whose restriction $\alpha:F\to G : D\to \mathcal{E}$ is [[equifibered natural transformation|equifibered]]. Let $p:V\to U$ be a universe classifying $\alpha_d : F_d \to G_d$ for each vertex $d\in D_0$. Then $\alpha$ is the pullback of $p$ along a cocone $q:G\to U$, yielding a cocone $r : \alpha \to p$ in $\mathcal{E}^\to$ which is equifibered.

Since $\alpha^\rhd$ is colimiting under $\alpha:D\to \mathcal{E}^\to$, we have an induced map $\alpha_\star \to p$, where $\star\in D^\rhd$ is the cocone vertex. But since colimits are pullback-stable, the pullback of $G^\rhd$ along $p$ is a colimiting cocone under $F$, and hence isomorphic to $F^\rhd$. Thus, $\alpha^\rhd$ is equifibered.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
There exists a [[natural numbers object]].

\end{theorem}
Intuitively, it seems as if $\Omega(S^1)$ (which can be constructed using finite limits and colimits) ought to be the [[integers]] and we should be able to construct the natural numbers from it; but it is unclear to the authors of this page how to do that. Instead, we can (using the impredicative subobject classifier) define the smallest subobject of an object classifier $p:V\to U$ that contains the initial object and is closed under taking coproducts with the terminal object. This is almost right, but it is not 0-truncated. We could 0-truncate it, but to get a universal property relative to all objects rather than only 0-truncated ones, we can instead impose structure making the objects rigid, such as a partial order or a graph. This argument is formalized in type theory \hyperlink{ConstructingNat}{here}; to be precise either it would have to be translated manually into category-theoretic language, or the above conjecture about interpreting type theory in an elementary $(\infty,1)$-topos would have to be proven.

\begin{theorem}
\label{}\hypertarget{}{}
There is an [[(n-connected, n-truncated) factorization system]].

\end{theorem}
The case $n=-1$ can be constructed impredicatively using the subobject classifier: internally, $\Vert A \Vert$ is the smallest [[truth value]] implied by $A$. Then we can induct on \emph{external} natural numbers, defining $\Vert A \Vert_{n+1}$ to be the $(-1)$-image of the composite $A \to U^A \to (U')^A$, where the second map is the $n$-truncation. Note that in general it ``goes up a universe level'', so that the $n$-truncation ``goes up $n+2$ universe levels''. However, unlike type theory, an elementary $(\infty,1)$-topos has no globally chosen tower of universes, so this doesn't literally make sense to say. What we can say is that with this construction, it is not clear whether we can find object classifiers that are \emph{closed} under the $n$-truncation.

However, \hyperlink{Rijke17}{(Rijke17)} shows (again in type theory) that using finite colimits and the natural numbers, the $(-1)$-truncation can be constructed without raising the universe level. Assuming (as always) that this can be translated into $(\infty,1)$-category theory, it implies that we \emph{can} find object classifiers closed under the $(-1)$-truncation, and hence (by induction) under the $n$-truncation for all $n$. Moreover, with a natural numbers object this induction can be performed internally, obtaining in particular object classifiers closed under the $n$-truncation for all $n$ at once.

It seems likely that the construction of [[W-types]] in any elementary 1-topos can be repeated in the $(\infty,1)$-case.

There is some structure that the definition probably does not imply, namely a semantic counterpart of arbitrary \emph{recursive} [[higher inductive types]], such as arbitrary [[localization]]. It is certain that these cannot always be constructed in an elementary 1-topos: for instance, HITs imply that all (even infinitary) [[algebraic theories]] have initial algebras, whereas this cannot be proven in [[ZF]] without the [[axiom of choice]] (under appropriate [[large cardinal]] hypotheses). Thus, it seems very unlikely that they can be constructed in an elementary $(\infty,1)$-topos. Moreover, it is even unclear exactly what $(\infty,1)$-categorical structure should correspond to arbitrary [[higher inductive types]], not least because we lack an accepted general definition of an ``arbitrary HIT''.

However, although this is an open question, it is arguably not a question about the definition of ``elementary $(\infty,1)$-topos'', but some stronger notion, analogous to a stronger notion of 1-topos that lacks an accepted name. Moreover, a great deal of [[homotopy type theory]] (including synthetic homotopy theory) can be done with only non-recursive HITs, truncations, and a natural numbers type, and even in the absence of a general coherence theorem any particular result of HoTT could probably be explicitly written down in $(\infty,1)$-categorical language.

\hypertarget{definition_predicative_case}{}\subsection*{{Definition (predicative case)}}\label{definition_predicative_case}

Since there is no consensus even on the definition of [[predicative topos|predicative 1-topos]], it seems less likely that there is a definitive answer for a predicative $(\infty,1)$-topos. However, it should probably include \emph{at least} the following axioms (which as we have seen above, are all true in the impredicative case although not included in the definition):

\begin{itemize}%
\item $E$ has finite [[(∞,1)-limit|limits and colimits]]
\item $E$ is [[locally cartesian closed (∞,1)-category|locally cartesian closed]]
\item For any finite family of morphisms $\{f_i:Y_i\to X_i\}_{i\in I}$, there exists a universe classifying each $f_i$.
\item $E$ has a [[natural numbers object]], and perhaps also [[W-types]].

\end{itemize}
Note that the stronger universe axiom implies, as above, that finite colimits are van Kampen, and in particular therefore that finite coproducts are disjoint. Instead of strengthening this axiom, we could assume explicitly that finite coproducts are disjoint, and then repeat the proof of descent given above.

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

There is presently no known example of an elementary $(\infty,1)$-topos which is not a [[Grothendieck (∞,1)-topos]], though there are some ideas.

\hypertarget{related_pages}{}\subsection*{{Related pages}}\label{related_pages}

\begin{itemize}%
\item [[elementary topos]]


\item [[predicative topos]]


\item [[Grothendieck (∞,1)-topos]], [[(∞,1)-pretopos]]


\item [[homotopy type theory]]


\item [[Awodey's conjecture]]



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

A vague version of the above proposed definition is on the very last slide of

\begin{itemize}%
\item [[Mike Shulman]], \emph{Inductive and higher inductive types} (2012) (\href{https://home.sandiego.edu/~shulman/hottminicourse2012/04induction.pdf}{pdf})

\end{itemize}
See also

\begin{itemize}%
\item [[Michael Shulman]], \emph{Towards elementary infinity-toposes}, Vladimir Voevodsky Memorial Conference, IAS, September 2018, \href{https://www.youtube.com/watch?v=ld4YL787dAk}{talk}.


\item [[Michael Shulman]], [[Peter Lumsdaine]], 2016, \emph{Semantics and syntax of higher inductive types}, (\href{http://home.sandiego.edu/~shulman/papers/stthits.pdf}{slides})


\item [[André Joyal]], \emph{What is an elementary higher topos?}, talk at \emph{\href{https://www.msri.org/workshops/689}{Reimagining The Foundations Of Algebraic Topology}} April 07, 2014 - April 11, 2014\_ \href{https://www.msri.org/workshops/689/schedules/18227}{web video} \href{https://www.msri.org/workshops/689/schedules/18227/documents/2046/assets/20468}{PDF} (slides 57-end). This lecture contains a proposed definition that is not an $(\infty,1)$-category but a presentation of one by a [[model category]]-like structure; this is closer to the type theory, but further from the intended examples. In particular, there are unresolved coherence questions even as to whether every Grothendieck $(\infty,1)$-topos can be presented by a model in Joyal's sense (in particular, how strict can a universe be made, and can the [[natural numbers object]] be made fibrant). Other than that, the main difference is that Joyal assumes only one fixed universe.


\item [[Georg Hegel]], \href{Science+of+Logic#LehreVomWesen}{book 2} of \emph{[[Science of Logic]]}



\end{itemize}
For an alternative definition proven (in Theorem 3.16) to be equivalent to the one given above, see

\begin{itemize}%
\item [[Nima Rasekh]], \emph{A Theory of Elementary Higher Toposes}, (\href{https://arxiv.org/abs/1805.03805}{arXiv:1805.03805})

\end{itemize}
The construction of $n$-truncations without recursive HITs is in

\begin{itemize}%
\item [[Egbert Rijke]], \emph{The join construction}, \href{https://arxiv.org/abs/1701.07538}{arxiv:1701.07538}

\end{itemize}
The construction of natural numbers from propositional resizing and univalence is in

\begin{itemize}%
\item HoTT/Coq library, \href{https://github.com/HoTT/HoTT/blob/master/theories/PropResizing/Nat.v}{https\char58\char47\char47github\char46com\char47HoTT\char47HoTT\char47blob\char47master\char47theories\char47PropResizing\char47Nat\char46v}

\end{itemize}
Results holding for elementary (∞,1)-toposes:

\begin{itemize}%
\item [[Nima Rasekh]], \emph{Yoneda Lemma for Elementary Higher Toposes}, (\href{https://arxiv.org/abs/1809.01736}{arXiv:1809.01736})


\item [[Nima Rasekh]], \emph{Every Elementary Higher Topos has a Natural Number Object}, (\href{https://arxiv.org/abs/1809.01734}{arXiv:1809.01734})


\item [[Nima Rasekh]], \emph{Truncations and Blakers-Massey in an Elementary Higher Topos}, (\href{https://arxiv.org/abs/1812.10527}{arXiv:1812.10527})



\end{itemize}
[[!redirects elementary (∞,1)-topos]] [[!redirects elementary (infinity,1)-topos]] [[!redirects elementary (∞,1)-toposes]] [[!redirects elementary (infinity,1)-toposes]] [[!redirects elementary infinity-topos]] [[!redirects elementary infinity-toposes]]

[[!redirects predicative elementary (∞,1)-topos]] [[!redirects predicative elementary (infinity,1)-topos]] [[!redirects predicative elementary (∞,1)-toposes]] [[!redirects predicative elementary (infinity,1)-toposes]] [[!redirects predicative elementary infinity-topos]] [[!redirects predicative elementary infinity-toposes]]



\end{document}