\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*{locally cartesian closed (infinity,1)-category}

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

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

[[!include quasi-category theory contents]]

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

\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{Properties}{Properties}\dotfill \pageref*{Properties} \linebreak
\noindent\hyperlink{Presentations}{Presentations}\dotfill \pageref*{Presentations} \linebreak
\noindent\hyperlink{InternalLogic}{Internal logic and homotopy type theory}\dotfill \pageref*{InternalLogic} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

An [[(∞,1)-category]] $C$ has [[finite limit|finite]] [[(∞,1)-limits]] if it has a [[terminal object in a quasi-category|terminal object]] and for every [[object]] $x \in C$, the [[over-(∞,1)-category]] $C_{/x}$ has finite [[products]].

We say that such a $C$ is \textbf{locally cartesian closed} if moreover $C_{/x}$ is a [[cartesian closed (∞,1)-category]] for every object $x$. This is equivalent to asking that the pullback functor $f^*\colon C_{\y} \to C_{\x}$, for any $f\colon x\to y$ in $C$, has a right adjoint $\Pi_f$.

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

\begin{itemize}%
\item Every (Grothendieck) [[(∞,1)-topos]] is locally cartesian closed. This follows from the [[universal colimit|universality of colimits]] and the [[adjoint functor theorem]].

\end{itemize}
\hypertarget{Properties}{}\subsection*{{Properties}}\label{Properties}

\hypertarget{Presentations}{}\subsubsection*{{Presentations}}\label{Presentations}

The following theorem should be compared with the fact that every [[locally presentable (∞,1)-category]] admits a presentation by a [[Cisinski model category]], indeed by a [[left Bousfield localization]] of a [[global model structure on simplicial presheaves]].

\begin{theorem}
\label{PresentationTheorem}\hypertarget{PresentationTheorem}{}
For a locally presentable $(\infty,1)$-category $C$, the following are equivalent.

\begin{enumerate}%
\item $C$ is locally cartesian closed.
\item [[(∞,1)-colimit|(∞,1)-Colimits]] in $C$ are [[universal colimits|stable under pullback]].
\item $C$ admits a presentation by a [[combinatorial model category|combinatorial]] [[locally cartesian closed model category]].
\item $C$ admits a presentation by a [[right proper model category|right proper]] [[Cisinski model category]].
\item $C$ admits a [[presentable (infinity,1)-category|presentation]] by a [[right proper model category|right proper]] [[Bousfield localization of model categories|left Bousfield localization]] of an [[model structure on simplicial presheaves|injective]] [[model structure on sSet-enriched presheaves]] over some small [[sSet-site]].

\end{enumerate}
\end{theorem}
\begin{proof}
Since [[left adjoints]] preserve colimits, the first condition implies the second. The converse holds by the [[adjoint functor theorem]] since each slice of $C$ is locally presentable.

Suppose $M$ is a right proper Cisinski model category. Then pullback along a fibration preserves cofibrations (since they are the monomorphisms) and weak equivalences (since $M$ is right proper). Since $M$ is a locally cartesian closed 1-category, pullback also has a right adjoint, so it is a [[Quillen adjunction|left Quillen functor]]; thus the fourth condition implies the third. Since left Quillen functors preserve homotopy colimits, the third condition implies the second.

The fifth condition implies the fourth, since the model structure therein is Cisinski. The only nonobvious part of this is that its underlying category is a topos, which follows from the fact that $sSet$-enriched presheaves on a $sSet$-enriched category $C$ can be identified with [[internal diagrams]] on $C$ regarded as an [[internal category]] in $sSet$, and the category of internal diagrams on any internal category in a topos (such as $sSet$) is again a topos.

It remains to show that the second condition implies the fifth. For that, see \href{http://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306}{this blog comment} by [[Denis-Charles Cisinski]]. An alternative proof can be found in \hyperlink{GepnerKock12}{(Gepner-Kock 12, Thm 7.10)}.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
Further equivalent characterizations of locally cartesian closed $(\infty,1)$-categories are in (\hyperlink{Lurie}{Lurie, prop. 6.1.1.4, lemma 6.1.3.3})

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
Comparing the third and the fifth item in theorem \ref{Presentations} notice that the projective and the injective [[model structure on simplicial presheaves]] are [[Quillen equivalence|Quillen equivalent]] (as discussed at \emph{[[model structure on functors]]}.)

\end{remark}
\hypertarget{InternalLogic}{}\subsubsection*{{Internal logic and homotopy type theory}}\label{InternalLogic}

It is expected that the [[internal logic]] of locally cartesian closed $(\infty,1)$-categories should be a sort of [[homotopy type theory]] (specifically, that with intensional [[identity types]] and [[dependent products]]), in higher analogy with the [[relation between type theory and category theory]]. More specifically, the following are hoped to be true:

\begin{itemize}%
\item From any type theory, its [[syntactic category]] is (or gives rise to) an $(\infty,1)$-category, which is the [[initial object]] in an appropriate $(\infty,1)$-category (or perhaps $(\infty,2)$-category) of locally cartesian closed $(\infty,1)$-categories (perhaps with additional structure corresponding to additional axioms or rules in the type theory). Thus, type theory can be ``interpreted'' in any lcc $(\infty,1)$-category by way of the universal morphism from this initial object.


\item From any locally cartesian closed $(\infty,1)$-category $C$, one can construct a type theory with rules or axioms corresponding to its objects and morphisms, which has a canonical interpretation in $C$ itself. This would be the ``internal language'' of $C$.


\item These construction should set up some sort of adjunction, or perhaps equivalence, between some $(\infty,1)$- or $(\infty,2)$-category of type theories and that of lcc $(\infty,1)$-categories.



\end{itemize}
Some partial results in these directions are known. For instance, Theorem \ref{Presentations} says in particular that every \emph{locally presentable} and locally cartesian closed $(\infty,1)$-category has a presentation by a [[type-theoretic model category]]. As discussed there, this provides [[categorical semantics]] for [[homotopy type theory]] (without in general the [[univalence]] [[axiom]]), at least if we assume the initiality of the syntactic 1-category (which is known in a special case and expected to be true in all cases). Together, this yields:

\begin{theorem}
\label{InterpretationTheoemForHoTT}\hypertarget{InterpretationTheoemForHoTT}{}
\textbf{(Cisinski, Shulman)} Assuming the initiality of the syntactic 1-category, every locally presentable locally cartesian closed $(\infty,1)$-category admits an interpretation of [[Martin-Löf type theory]] with [[dependent sum types]], [[dependent product types]], and [[identity types]] (``[[homotopy type theory]]'').

Moreover it also interprets [[function extensionality]] (\hyperlink{Shulman12}{Shulman 12, lemma 5.9}, see this \href{function+extensionality#EveryPresentableLocallyCartesinClosedInfinityCatInterpretsHoTTPlusFunExt}{this discussion}.

Hence every presentable locally cartesian closed $\infty$-category interprets [[HoTT]]+[[FunExt]].

\end{theorem}
This includes in particular all ([[∞-stack]]-) [[(∞,1)-toposes]]. The latter should in addition possess [[univalence|univalent universes]], but that is at present known only weakly except for a restricted class. See also \emph{[[internal logic of an (∞,1)-topos]]}.

This statement is not fully satisfactory for several reasons. Firstly, it assumes local presentability. Secondly, rather than staying in the world of $(\infty,1)$-categories, it goes by way of a strict presentation. Thus, the existence and behavior of a ``universal model'' is unclear.

A step in the latter direction was conjectured in (\hyperlink{Joyal11}{Joyal 2011}), and established in [[Chris Kapulkin]]`s PhD thesis (see \hyperlink{Kapulkin14}{Kapulkin 14}, \hyperlink{Kapulkin15}{Kapulkin 15}):

\begin{theorem}
\label{}\hypertarget{}{}
\textbf{(Kapulkin)} If \textbf{T} is any [[dependent type theory]] with (at least) $\Sigma$-types, $\Pi$-types, and $\mathrm{Id}$-types, then the [[simplicial localisation]] of its [[syntactic category|classifying category]] $\mathrm{Cl}(\mathbf{T})$ is a locally cartesian closed $(\infty,1)$-category.

\end{theorem}
However, this ``syntactic $(\infty,1)$-category'' will not in general be locally presentable, lacking appropriate colimits. There is thus a mismatch between the two best statements we have at present, for the two directions of the internal language correspondence.

Furthermore, nothing is yet known about the \emph{initiality} of this syntactic $(\infty,1)$-category, which is a central aspect of what it means to have an internal language. Finally, no one has yet explicitly constructed an ``internal language'' type theory from an $(\infty,1)$-category, and so of course the desired adjunction/equivalence cannot yet even be stated as a precise conjecture.

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

\begin{itemize}%
\item [[cartesian closed category]], [[locally cartesian closed category]]


\item [[cartesian closed functor]], [[locally cartesian closed functor]]


\item [[cartesian closed model category]], [[locally cartesian closed model category]]


\item [[cartesian closed (∞,1)-category]], \textbf{locally cartesian closed (∞,1)-category}



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

Characterizations of locally presentable locally cartesian closed $(\infty,1)$-categories (as [[locally presentable (∞,1)-categories]] with [[universal colimits]]) are discussed in section 6.1 of

\begin{itemize}%
\item [[Jacob Lurie]], \emph{[[Higher Topos Theory]]}

\end{itemize}
Early discussion in the context of [[homotopy type theory]] is

\begin{itemize}%
\item [[André Joyal]], \emph{Remarks on homotopical logic}, Oberwolfach (2011) (\href{http://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf#page=19}{pdf})

\end{itemize}
proposing [[homotopy type theory]] as an internal language for locally cartesian closed $\infty$-categories ([[Awodey's conjecture]]).

[[Denis-Charles Cisinski]]`s argument in Theorem \ref{Presentations} above, that every locally presentable locally cartesian closed $(\infinity,1)$-category admits a presentation by a [[type-theoretic model category]], originally appeared on the Caf\'e{} (\href{http://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306}{this blog comment}) and is mentioned in print in Examples 2.16 of

\begin{itemize}%
\item [[Michael Shulman]], \emph{Univalence for inverse diagrams and homotopy canonicity}, Mathematical Structures in Computer Science, Volume 25, Issue 5 ( \emph{From type theory and homotopy theory to Univalent Foundations of Mathematics} ) June 2015 (\href{https://arxiv.org/abs/1203.3253}{arXiv:1203.3253}, \href{https://doi.org/10.1017/S0960129514000565}{doi:/10.1017/S0960129514000565})

\end{itemize}
which gives a detailed account of the categorical semantics of homotopy type theory in [[type-theoretic model categories]] such as those presenting locally cartesian closed $(\infty,1)$-categories.

For more on this see also the relevant sections at \emph{[[relation between type theory and category theory]]}.

Discussion of the converse direction, obtaining locally cartesian closed $(\infty,1)$-categories as [[syntactic categories]] of [[homotopy type theory|homotopy type theories]] is in

\begin{itemize}%
\item [[Chris Kapulkin]], \emph{Type theory and locally cartesian closed quasicategories}, Oxford 2014 (\href{https://www.youtube.com/watch?v=g87bZJ2bvYk}{video})


\item [[Chris Kapulkin]], \emph{Locally Cartesian Closed Quasicategories from Type Theory} (\href{http://arxiv.org/abs/1507.02648}{arXiv:1507.02648})



\end{itemize}
A discussion of object classifiers, univalent families, and model category presentations is the context of $(\infty,1)$-categories (and hence in categorical semantics for what should be homotopy type theory with univalent universes ``weakly a la Tarski'') appeared also in

\begin{itemize}%
\item [[David Gepner]], [[Joachim Kock]], ``Univalence in locally cartesian closed ∞-categories'', \href{http://arxiv.org/abs/1208.1749}{arXiv}

\end{itemize}
[[!redirects locally cartesian closed (∞,1)-category]] [[!redirects locally cartesian closed (infinity,1)-categories]] [[!redirects locally cartesian closed (∞,1)-categories]]

[[!redirects locally Cartesian closed (∞,1)-category]] [[!redirects locally Cartesian closed (∞,1)-categories]] [[!redirects locally Cartesian closed (infinity,1)-category]] [[!redirects locally Cartesian closed (infinity,1)-categories]]

[[!redirects locally Cartesian closed infinity,1-category]] [[!redirects locally Cartesian closed infinity,1-categories]]



\end{document}