\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*{internal logic of an (infinity,1)-topos}

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

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

[[!include type 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{type_theory_versus_logic}{Type theory versus logic}\dotfill \pageref*{type_theory_versus_logic} \linebreak
\noindent\hyperlink{the_type_theory_of_an_category}{The type theory of an $(\infty,1)$-category}\dotfill \pageref*{the_type_theory_of_an_category} \linebreak
\noindent\hyperlink{intensional_identity_types_in_categories}{Intensional identity types in $(\infty,1)$-categories}\dotfill \pageref*{intensional_identity_types_in_categories} \linebreak
\noindent\hyperlink{additional_axioms}{Additional axioms}\dotfill \pageref*{additional_axioms} \linebreak
\noindent\hyperlink{logic_over_type_theory_in_an_category}{Logic over type theory in an $(\infty,1)$-category}\dotfill \pageref*{logic_over_type_theory_in_an_category} \linebreak
\noindent\hyperlink{the_problem_of_finiteness}{The problem of finiteness}\dotfill \pageref*{the_problem_of_finiteness} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{OfInfGrpd}{Internal logic in $\infty Grpd$}\dotfill \pageref*{OfInfGrpd} \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}

Just as an ordinary [[elementary topos]] comes with its [[internal logic]] formalized by [[type theory]], an [[elementary (∞,1)-topos]] should come with its \emph{internal ``$(\infty,1)$-logic''} formalized by [[homotopy type theory]].

\hypertarget{type_theory_versus_logic}{}\subsection*{{Type theory versus logic}}\label{type_theory_versus_logic}

As remarked at [[type theory]], it is useful to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing [[subobjects]]. For instance, [[limits]] and [[colimits]], [[exponential object|exponentials]], and [[object classifiers]] belong to the type theory, while [[images]], [[dual image|dual images]], [[intersections]], [[unions]], and [[subobject classifiers]] belong to the logic. Thus, the semantics of (extensional) type theory naturally lies in a category with appropriate structure, while the semantics of logic over that type theory naturally lies in some indexed [[poset]] over that category. However, we commonly take this indexed poset to consist of the [[subobjects]] in the category in question, in which case additional ``logical'' structure on the category is required, for instance that it be a [[Heyting category]].

In an elementary 1-topos, all of the ``logical'' structure is not usually included in the definition, because it comes for free once you have [[power objects]]. But object classifiers may not be as powerful as power objects in this respect, so for purposes of studying the internal logic (and not just the internal type theory) of an $(\infty,1)$-topos, it's good to keep in mind both the type-theoretic structure and the logical structure, and in particular both the object classifier and the subobject classifier.

\hypertarget{the_type_theory_of_an_category}{}\subsection*{{The type theory of an $(\infty,1)$-category}}\label{the_type_theory_of_an_category}

Amazingly, a variant of type theory that seems appropriate for interpretation in an $(\infty,1)$-category already exists, namely \emph{intensional type theory} with [[identity type]]s.

\hypertarget{intensional_identity_types_in_categories}{}\subsubsection*{{Intensional identity types in $(\infty,1)$-categories}}\label{intensional_identity_types_in_categories}

The usual sort of type theory that one interprets in a 1-category is \emph{extensional type theory}. To explain what this means, consider how the categorical structure of finite limits is represented in the type theory. On the one hand, we have product types $A\times B$, which of course represent categorical [[products]]; thus to obtain finite limits it suffices to have [[equalizers]]. We can obtain these from \emph{identity types}, which supply for each type $A$ and each pair of terms $x,y:A$, a dependent type $Id_A(x,y)$, whose intended interpretation is that it is inhabited precisely when $x=y$. In terms of 1-categorical semantics, it is natural to require that any two elements of $Id_A(x,y)$ be equal, i.e. that $Id_A(x,y)$ be essentially a [[truth value]]/[[subsingleton]]. Then if we have two terms $x:A\vdash f(x):B$ and $x:A\vdash g(x):B$ representing morphisms $f,g\colon A\to B$, their equalizer is represented by the type $\Sigma_{x:A} Id_B(f(x),g(x))$.

However, for semantics in an $(\infty,1)$-category, it makes sense to use the same identity types, but now interpreted as a [[path space]]. Now it will no longer be true that $Id_A(x,y)$ is a subsingleton, since two points can be connected by more than one path, so we must drop that axiom. This \emph{intensional type theory} has been widely studied by type-theorists, although from a different point of view: assuming the [[propositions as types]] approach, $Id_A(x,y)$ should be the type of \emph{proofs} or \emph{reasons} why $x=y$, which can also of course have many different elements.

Thus we suspect that intensional type theory may be a natural sort of type theory to have semantics in an $(\infty,1)$-category. According to the general framework of syntax/semantics, we would hope that

\begin{enumerate}%
\item From any intensional type theory, we can construct a syntactic $(\infty,1)$-category, and
\item In any $(\infty,1)$-category, we can model an intensional type theory.

\end{enumerate}
Some work in both of these directions has been done. On the one hand, it is known that in any intensional type theory with identity types, for any type $A$ the [[globular set]] (or more accurately globular [[context]]) given by

\begin{displaymath}
A \leftleftarrows Id_A \leftleftarrows Id_{Id_A} \leftleftarrows \dots
\end{displaymath}
has the structure of a [[Batanin ∞-groupoid]]. This can be found in:

\begin{itemize}%
\item [[Peter Lumsdaine]], \emph{Weak omega-categories from intensional type theory}, \href{http://arxiv.org/abs/0812.0409}{arXiv:0812.0409}, and independently
\item [[Richard Garner]] and [[Benno van den Berg]], \emph{Types are weak omega-groupoids}, \href{http://arxiv.org/abs/0812.0298}{arXiv:0812.0298}).

\end{itemize}
Moreover, the syntactic category of such a theory carries a natural [[weak factorization system]], the [[identity type weak factorization system]]. However, there seems as yet to be no published work constructing a full syntactic $(\infty,1)$-category.

On the other hand, it is known that in any nice enough [[model category]] (and in fact, in any category with a nice enough [[weak factorization system]]), one can model intensional type theory. This is studied in

\begin{itemize}%
\item [[Steve Awodey]] and [[Michael Warren]], \emph{Homotopy theoretic models of identity types}, \href{http://arxiv.org/abs/0709.0248}{arXiv:0709.0248}
\item [[Michael Warren]], \emph{Homotopy theoretic aspects of constructive type theory}, \href{http://aix1.uottawa.ca/~mwarren/Papers/phd.pdf}{Ph.D. thesis}.

\end{itemize}
[[Vladimir Voevodsky]] has also studied the particular model of intensional type theory in simplicial sets, which he calls the \emph{univalent model}; see his \href{http://www.math.ias.edu/~vladimir/Site3/home.html}{website}.

\hypertarget{additional_axioms}{}\subsubsection*{{Additional axioms}}\label{additional_axioms}

Although intensional type theory has semantics in $(\infty,1)$-categories, one can naturally expect that these models will all satisfy additional axioms. This is especially true if we want to add additional structure to our $(\infty,1)$-categories.

\begin{itemize}%
\item Exponential (and dependent product) types can probably be modeled by (locally) cartesian closed $(\infty,1)$-categories. However, although exponentials in an $(\infty,1)$-category are not strictly extensional the way they are in a 1-category, they are still extensional ``up to coherent higher homotopies,'' which (unlike the case for identity types) is seemingly not guaranteed by the type-theoretic structure. Thus, there may be an $\infty$-extensionality axiom to be added.


\item Disjoint sum types may be expected to correspond to coproducts in an $(\infty,1)$-category.


\item The usual notions of \emph{quotient type} make little sense without extensional identity types. In the 1-categorical world, quotient types correspond to [[exact categories]], while the appropriate notion of ``exactness'' for an $(\infty,1)$-category deals with [[groupoid objects in an (∞,1)-category]]. It remains to be seen how to phrase a corresponding axiom in the type theory.


\item The [[object classifier]] in an $(\infty,1)$-topos does in fact correspond to a well-known concept in type theory, namely that of a \emph{universe} such as the type $Type$. However, as a universe, the object classifier in an $(\infty,1)$-topos has the special property that the \emph{paths} between two types $A$ and $B$ as elements of $Type$ (that is, the path space $Id_{Type}(A,B)$) is equivalent to the space of equivalences between $A$ and $B$ as types (an appropriate subspace of the exponential $B^A$). A type-theoretic axiom asserting this equivalence was introduced by [[Vladimir Voevodsky|Voevodsky]] under the name of the \emph{equivalence axiom}.



\end{itemize}
\hypertarget{logic_over_type_theory_in_an_category}{}\subsection*{{Logic over type theory in an $(\infty,1)$-category}}\label{logic_over_type_theory_in_an_category}

Now when we go to add \emph{logic} to the type theory of an $(\infty,1)$-category, it seems natural by analogy that it will deal with \emph{subobjects}, i.e. with [[monomorphisms in an (∞,1)-category]]. That is, a proposition $\varphi(x)$ with a variable $x:A$ will be interpreted by a monomorphism $[\varphi] \rightarrowtail [A]$. Just as in the [[internal logic]] of a 1-category and of a [[michaelshulman:2-categorical logic|2-category]], in order to interpret the logical connectives and quantifiers we will then need suitable structure on the posets of subobjects in our $(\infty,1)$-category. It is naturally to be expected that any $(\infty,1)$-topos will have this necessary structure.

Again, the requisite type theory more or less exists, namely intensional type theory together with a sort of propositions that can depend on types. In fact, this type theory is very closely related to the [[calculus of constructions]] used in the proof assistant \href{http://coq.inria.fr/}{Coq}, making Coq a very convenient place to play around with the type theory that ought to be valid in an $(\infty,1)$-topos. In particular, Voevodsky has written out a Coq script up to the statement of his equivalence axiom, to be found on his \href{http://www.math.ias.edu/~vladimir/Site3/home.html}{website}.

\hypertarget{the_problem_of_finiteness}{}\subsection*{{The problem of finiteness}}\label{the_problem_of_finiteness}

In describing the internal type theory and logic of an $(\infty,1)$-category we encounter the problem that many structures in an $(\infty,1)$-category require a (countably) infinite amount of data to describe. For instance, when looking for a way to state the ``exactness'' property one has to say what is meant by a groupoid object, but since this really means a ``coherent'' or ``$A_\infty$'' groupoid object, it involves an infinite amount of data. By contrast, the most common type theories are purely finitary systems.

There is the one amazing fact that the entire complicated infinitary structure of a Batanin $\omega$-groupoid can be recovered from the simple finitary rules of identity types. It is not clear, however, whether we can expect this happy occurrence to continue. We might have to bite the bullet and work with an infinitary type theory, i.e. one allowing derivation rules taking as input an infinite list of hypotheses. In fact, this is almost certainly what we will need if we want a good notion of a [[geometric theory]] in the $(\infty,1)$-case, since that involves infinitary logic even in the 1-categorical case.

However, such a type theory would obviously no longer have ``computational content'' and couldn't be modeled in a proof assistant such as Coq, and also wouldn't provide a fully ``elementary,'' i.e. finitary first-order, theory such as [[ETCS]] provides in the 1-categorical case. It might be helpful to note that infinitary structures can at least sometimes be finitarily described using [[inductive type]]s and/or [[coinductive type]]s, but it is not clear yet whether this is useful in the $(\infty,1)$-categorical context.

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

\hypertarget{OfInfGrpd}{}\subsubsection*{{Internal logic in $\infty Grpd$}}\label{OfInfGrpd}

The archetypical [[(∞,1)-topos]] is [[∞Grpd]]. This is to be thought of as the [[vertical categorification|(∞,1)-categorification]] of the archetypical 1-[[topos]] [[Set]].

At \href{http://ncatlab.org/nlab/show/internal+logic#LogicOfSet}{internal logic - in Set} is a step-by-step discussion of how ordinary logic is recovered from the point of view of the [[internal logic]] of a topos $\mathcal{T}$ when choosing $\mathcal{T} := Set$.

Here we look at the $(\infty,1)$-categorical analog of that discussion, step-by-step, now everything internal to [[∞Grpd]].

\begin{itemize}%
\item The [[terminal object]] of $\infty Grpd$ is [[generalized the|the]] [[contractible]] $\infty$-groupoid $*$.

This \emph{generates} $\infty Grpd$ under [[colimit]]s: every small $\infty$-groupoid is a colimit over a small diagram consisting only of copies of the terminal $\infty$-groupoid.


\item The \emph{subobject classifier} of $\infty Grpd$ is

$\Omega = \{\top, \bottom\}$

The \emph{object} classifier should be the [[core]] of the [[universal fibration of (infinity,1)-categories|universal left fibration]].

See [[(sub)object classifier in an (∞,1)-topos]].



\end{itemize}
Now\ldots{}

\ldots{}

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

\begin{itemize}%
\item [[internal logic]], [[type theory]]


\item \textbf{internal logic in an $(\infty,1)$-topos}, [[homotopy type theory]]



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

\begin{itemize}%
\item [[Chris Kapulkin]], \emph{Internal Languages of Higher Categories}, \href{https://golem.ph.utexas.edu/category/2015/07/internal_languages_of_higher_c.html}{blog post}


\item [[Chris Kapulkin]], \emph{Internal Languages of Higher Categories II}, \href{https://golem.ph.utexas.edu/category/2017/11/internal_languages_of_higher_c_1.html}{blog post} [[!redirects internal logic of an (∞,1)-topos]]



\end{itemize}


\end{document}