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

\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{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{for_fibrations_in_groupoids}{For fibrations in $\infty$-groupoids}\dotfill \pageref*{for_fibrations_in_groupoids} \linebreak
\noindent\hyperlink{GrpdModelCatVersion}{Model category presentation}\dotfill \pageref*{GrpdModelCatVersion} \linebreak
\noindent\hyperlink{GrpdFibsOverGrpds}{Remark: $(\infty,0)$-fibrations over an $\infty$-groupoid}\dotfill \pageref*{GrpdFibsOverGrpds} \linebreak
\noindent\hyperlink{for_general_fibered_categories}{For general fibered $(\infty,1)$-categories}\dotfill \pageref*{for_general_fibered_categories} \linebreak
\noindent\hyperlink{ModCatCart}{Model category presentation}\dotfill \pageref*{ModCatCart} \linebreak
\noindent\hyperlink{OverCat}{Over an ordinary category}\dotfill \pageref*{OverCat} \linebreak
\noindent\hyperlink{relation_beween_the_model_structures}{Relation beween the model structures}\dotfill \pageref*{relation_beween_the_model_structures} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{as_an_oplax_colimit}{As an (op)lax $\infty$-colimit}\dotfill \pageref*{as_an_oplax_colimit} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{cartesian_fibrations_over_the_point}{Cartesian fibrations over the point}\dotfill \pageref*{cartesian_fibrations_over_the_point} \linebreak
\noindent\hyperlink{FibsOverInterval}{Cartesian fibrations over the interval}\dotfill \pageref*{FibsOverInterval} \linebreak
\noindent\hyperlink{CartOverSimplex}{Cartesian fibrations over simplices}\dotfill \pageref*{CartOverSimplex} \linebreak
\noindent\hyperlink{the_universal_cartesian_fibration}{The universal Cartesian fibration}\dotfill \pageref*{the_universal_cartesian_fibration} \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{$(\infty,1)$-Grothendieck construction} is a generalization of the [[Grothendieck construction]] -- which establishes an equivalence

\begin{displaymath}
Fib(C) \simeq 2Func(C^{op}, Cat)
\end{displaymath}
and

\begin{displaymath}
Fib_{Grpd}(C) \simeq 2Func(C^{op}, Grpd)
\end{displaymath}
between [[fibered category|fibered categories]]/[[categories fibered in groupoids]] and [[pseudofunctor]]s to [[Cat]]/to [[Grpd]] -- from [[category theory]] to [[(∞,1)-category]]-[[higher category theory|theory]].

The Grothendieck construction for [[∞-groupoid]]s constitutes an equivalence of [[(∞,1)-categories]]

\begin{displaymath}
RFib(C) \simeq \infty Func(C^{op}, \infty Grpd)
\end{displaymath}
between [[right fibration]]s [[fibrations of quasi-categories|of quasi-categories]] and [[(∞,1)-functor]]s to [[? Grpd]], while the full Grothendieck construction for [[(∞,1)-categories]] constitutes an equivalence

\begin{displaymath}
CartFib(C) \simeq \infty Func(C^{op}, (\infty,1)Cat)
\end{displaymath}
between [[Cartesian fibration]]s [[fibrations of quasi-categories|of quasi-categories]] and [[indexed (∞,1)-categories]], that is, [[(∞,1)-functor]]s to [[(∞,1)Cat]].

This correspondence may be [[model category|modeled]]

\begin{itemize}%
\item in the case of $\infty$-groupoids by a [[Quillen equivalence]] between the [[model structure for right fibrations]] and the projective [[global model structure on simplicial presheaves]]


\item in the case of $(\infty,1)$-categories by a Quillen equivalence between the [[model structure for Cartesian fibrations]] and the [[global model structure on functors]] with values in the [[model structure on marked simplicial over-sets|model structure on marked simplicial sets]].



\end{itemize}
\hypertarget{for_fibrations_in_groupoids}{}\subsection*{{For fibrations in $\infty$-groupoids}}\label{for_fibrations_in_groupoids}

The generalization of a [[category fibered in groupoids]] to [[quasi-category]] theory is a [[right fibration|right]] [[fibrations of quasi-categories|fibration of quasi-categories]].

\begin{utheorem}
\textbf{($(\infty,0)$-Grothendieck construction)}

Let $C$ be an [[(∞,1)-category]]. There is an equivalence of [[(∞,1)-categories]]

\begin{displaymath}
RFib(C) \simeq Func(C^{op}, \infty Grpd)
\end{displaymath}
where

\begin{itemize}%
\item on the left we have the [[right fibration|(∞,1)-category of right fibrations]] $RFib(C)$ -- incarnated as the full [[SSet]]-[[subcategory]] of the [[overcategory]] $SSet/C$ on [[right fibration]]s;


\item and on the right the [[(∞,1)-category of (∞,1)-functors]] from the [[opposite category]] $C^{op}$ to [[∞Grpd]], i.e. the [[(∞,1)-category of (∞,1)-presheaves]] on $C$.



\end{itemize}
\end{utheorem}
In the next section we discuss how this statement is presented in terms of [[model categories]].

\hypertarget{GrpdModelCatVersion}{}\subsubsection*{{Model category presentation}}\label{GrpdModelCatVersion}

We discuss a [[presentable (∞,1)-category|presentation]] of the $(\infty,0)$-Grothendieck construction by a [[simplicial Quillen adjunction]] between [[simplicial model categories]]. ([[Higher Topos Theory|HTT, section 2.2.1]]).

\begin{udef}
\textbf{(extracting a simplicial presheaf from a fibration)}

Let

\begin{itemize}%
\item $S$ be a [[simplicial set]], $\tau_hc(S)$ the corresponding [[SSet-category]] (under the [[left adjoint]] $\tau_{hc} : SSet \to SSet Cat$ of the [[homotopy coherent nerve]], denoted $\mathfrak{C}$ in [[Higher Topos Theory|HTT]]);


\item $C$ an [[SSet-category]];


\item $\phi : \tau_{hc}(S) \to C$ a morphism of [[SSet-categories]].



\end{itemize}
\begin{quote}%
In particular we will be interested in the case that $\phi$ is the identity, or at least an equivalence, identifying $C$ with $\tau_{hc}(S)$.


\end{quote}
For any object $(p : X\to S)$ in $sSet/S$ consider the [[sSet-category]] $K(\phi,p)$ obtained as the (ordinary) [[pushout]] in [[SSet Cat]]

\begin{displaymath}
\itexarray{
    \tau_{hc}(X) &\stackrel{}{\to}& \tau_{hc}(X^{\triangleright})
    \\
    {}^{\mathllap{\phi(p)}}\downarrow && \downarrow
    \\
    C &\to& K(\phi,p) 
  }
  \,,
\end{displaymath}
where $X^{\triangleright} = X \star \{v\}$ is the [[join of simplicial sets]] of $X$ with a single vertex $v$.

Using this construction, define a functor, the \textbf{[[straightening functor]]},

\begin{displaymath}
St_\phi : sSet/S \to [C^{op}, sSet]
\end{displaymath}
from the [[overcategory]] of [[sSet]] over $S$ to the [[enriched functor category]] of [[sSet]]-[[enriched functor]]s from $C^{op}$ to $sSet$ by defining it on objects $(p : X \to S)$ to act as

\begin{displaymath}
St_\phi(X) := K(\phi,p)(-,v) : C^{op} \to SSet
  \,.
\end{displaymath}
\end{udef}
\begin{uexample}
The straightening functor effectively computes the fibers of a [[Cartesian fibration]] $(p : X \to C)$ over every point $x \in C$. As an illustration for how this is expressed in terms of morphisms in that pushout, consider the simple situation where

\begin{itemize}%
\item $C = *$ only has a single point;


\item $X = \left\{ a \to b \;\;\; c\right\}$ is a category with three objects, two of them connected by a morphism


\item $p : X\to C$ is the only possible functor, sending everything to the point.



\end{itemize}
Then

\begin{itemize}%
\item $X^{\triangleright} = 
  \left\{
    \itexarray{
    a &\to& b && c
    \\
    & \searrow \Leftarrow& \downarrow & \swarrow
    \\
    && v
    }
  \right\}$

\end{itemize}
and

\begin{itemize}%
\item $X^{\triangleright} \coprod_{X} C = 
  \left\{
    \itexarray{
    && \bullet
    \\
    & \swarrow & \downarrow & \searrow
    \\
    \downarrow& \Leftarrow & \downarrow
    \\
    & \searrow & \downarrow & \swarrow
    \\
    && v
    }
  \right\}$

\end{itemize}
Therefore the category of morphisms in this pushout from $*$ to $v$ is indeed again the category $\{a \to b \;\;\; c\}$.

More on this is at [[Grothendieck construction]] in the section of adjoints to the Grothendieck construction.

\end{uexample}
\begin{uprop}
With the definitions \hyperlink{UnmarkedStraighteningFunctor}{as above}, let $\pi : C \to C'$ be an [[sSet]]-[[enriched functor]] between [[sSet-categories]]. Write

\begin{displaymath}
\pi_! : [C^{op}, sSet] \to [{C'}^{op}, sSet]
\end{displaymath}
for the left [[sSet]]-[[Kan extension]] along $\pi$.

There is a [[natural isomorphism]] of the straightening functor for the composite $\pi \circ \phi$ and the original straightening functor for $\phi$ followed by left [[Kan extension]] along $\pi$:

\begin{displaymath}
St_{\pi \circ \phi} \simeq \pi_! \circ St_\phi
  \,.
\end{displaymath}
\end{uprop}
This is [[Higher Topos Theory|HTT, prop. 2.2.1.1.]]. The following proof has kindly been spelled out by [[Harry Gindi]].

\begin{proof}
We unwind what the [[sSet-categories]] with a single object adjoined to them look like:

let

\begin{displaymath}
F : C^{op} \to sSet
\end{displaymath}
be an [[sSet]]-[[enriched functor]]. Define from this a new [[sSet-category]] $C_F$ by setting

\begin{itemize}%
\item $Obj(C_F) = Obj(C) \coprod \{\nu\}$


\item $C_F(c,d) = \left\{
  \itexarray{
    C(c,d) & for c,d \in Obj(C)
    \\
    F(c) & for c \in Obj(c) and d = \nu
    \\
    \emptyset & for c = \nu and d \in Obj(C)
    \\
    * & for c = d = \nu
  }
\right.$



\end{itemize}
The composition operation is that induced from the composition in $C$ and the enriched functoriality of $F$.

Observe that the [[sSet-category]] $K(\phi,p)$ appearing in the \hyperlink{UnmarkedStraighteningFunctor}{definition of the straightening functor} is

\begin{displaymath}
K(\phi,p) \simeq C_{St_\phi(X)}
\end{displaymath}
(because $K(\phi,p)$ is $C$ with a single object $\nu$ and some morphisms to $\nu$ adjoined, such that there are no non-degenerate morphisms originating at $\nu$, we have that $K(\phi,p)$ is of form $C_F$ for some $F$; and $St_\phi(X)$ is that $F$ by definition).

To prove the proposition, we need to compute the pushout

\begin{displaymath}
\itexarray{
    \tau_{hc}(X) &\to& \tau_{hc}(X^{\triangleright})
    \\
    \downarrow && \downarrow
    \\
    C &\to& K(\phi,p) = C_{St_\phi(X)} 
    \\
   {}^{\mathllap{\pi}}\downarrow && \downarrow
   \\
   C' &\to& Q 
  }
\end{displaymath}
and show that indeed $Q \simeq C'_{\pi_! St_\phi(X)}$.

Using the pasting law for [[pushout]]s (see [[pullback]]) we just have to compute the lower square pushout. Here the statement is a special case of the following statement: for every [[sSet-category]] of the form $C_F$, the pushout of the canonical inclusion $C\to C_F$ along any $sSet$-functor $\pi : C \to C'$ is $C'_{\pi_! F}$.

This follows by inspection of what a cocone

\begin{displaymath}
\itexarray{
     C &\stackrel{\iota}{\to}& C_F
     \\
     {}^{\mathllap{\pi}}\downarrow && \downarrow^{\mathrlap{d}}
     \\
     C' &\underset{r}{\to}& Q 
  }
\end{displaymath}
is like: by the nature of $C_F$ the functor $d$ is characterized by a functor $d|_C : C \to Q$, an object $d(\nu) \in Q$ together with a [[natural transformation]]

\begin{displaymath}
F(c) \to  Q(d|_C(c), d(\nu))
\end{displaymath}
being the component $F_{c,\nu} : C_F(c,\nu) \to Q(d(c), d(\nu))$ of the $sSet$-functor.

We may write this natural transformation as

\begin{displaymath}
F \to (d|_C)^* Q(-,d(\nu)) = \iota^* d^* \nu Q(-,d(\nu))
  \,,
\end{displaymath}
where $d^*$ etc. means precomposition with the functor $d$.

By commutativity of the diagram this is

\begin{displaymath}
\cdots \simeq \pi^* r^* Q(-,d(\nu))
  \,.
\end{displaymath}
Now by the definition of left [[Kan extension]] $\pi_!$ as the [[left adjoint]] to prescomposition with a functor, this is bijectively a transformation

\begin{displaymath}
\eta : \pi_! F \to r^* Q(-,d(\nu))
  \,.
\end{displaymath}
Using this we see that we may find a universal cocone by setting $Q := C'_{\pi_! F}$ with $r : C' \to Q$ the canonical inclusion and $C_{F} \to C'_{\pi_! F}$ given by $\pi$ on the restriction to $C$ and by the [[unit of an adjunction|unit]] $F \to \pi^* \pi_! F$ on $C_F(c,\nu)$. For this the [[adjunct]] transformation $\eta$ is the identity, which makes this universal among all cocones.

\end{proof}
\begin{uprop}
This functor has a [[right adjoint]]

\begin{displaymath}
Un_\phi : [C^{op}, sSet] \to sSet/S
  \,,
\end{displaymath}
that takes a [[simplicial presheaf]] on $C$ to a simplicial set over $S$ -- this is the \textbf{unstraightening functor}.

\end{uprop}
\begin{proof}
One checks that $St_\phi$ preserves [[colimit]]s. The claim then follows with the [[adjoint functor theorem]].

\end{proof}
\begin{utheorem}
\textbf{(presentation of the $(\infty,0)$-Grothendieck construction)}

The straightening and the unstraightening functor constitute a [[Quillen adjunction]]

\begin{displaymath}
(St_\phi \dashv Un_\phi) : sSet/S
  \stackrel{\overset{Un_{\phi}}{\leftarrow}}{\underset{St_\phi}{\to}}
  [C^{op}, sSet]
\end{displaymath}
between the [[model structure for right fibrations]] and the global projective [[model structure on simplicial presheaves]] on $S$.

If $\phi$ is a weak equivalence in the [[model structure on simplicial categories]] then this Quillen adjunction is a [[Quillen equivalence]].

\end{utheorem}
This is [[Higher Topos Theory|HTT, theorem 2.2.1.2]].

This models the Grothendieck construction for [[∞-groupoid]]s in the following way:

\begin{itemize}%
\item the [[presentable (∞,1)-category|(∞,1)-category presented by]] $sSet/S$ is $RFib(S)$

([[Higher Topos Theory|HTT, lemma 2.2.3.9]])


\item the [[presentable (∞,1)-category|(∞,1)-category presented by]] the global [[model structure on simplicial presheaves]] $[C^{op}, SSet]$ is [[(∞,1)-category of (∞,1)-presheaves]] $PSh_{(\infty,1)}(N_{hc}(C))$



\end{itemize}
Hence the unstraightening functor is what models the [[Grothendieck construction]] proper, in the sense of a construction that generalizes the construction of a [[fibered category]] from a [[pseudofunctor]].

\hypertarget{GrpdFibsOverGrpds}{}\subsubsection*{{Remark: $(\infty,0)$-fibrations over an $\infty$-groupoid}}\label{GrpdFibsOverGrpds}

\begin{ulemma}
Let $C$ itself be an $\infty$-groupoid. Then $RFib(C) \simeq \infty Grpd/C$ and hence

\begin{displaymath}
\infty Grpd/C \simeq [C^{op}, \infty Grpd]
  \,.
\end{displaymath}
\end{ulemma}
\begin{proof}
By the fact that there is the standard [[model structure on simplicial sets]] we have that every morphism of $\infty$-groupoids $X \to C$ factors as

\begin{displaymath}
\itexarray{
     X &&\stackrel{\simeq}{\to}&& \hat X
     \\
     & \searrow && \swarrow_{\mathrlap{fib}}
     \\
     && C
  }
  \,,
\end{displaymath}
where the top morphism is an equivalence and the right morphism a [[Kan fibration]]. Moreover, as discussed at [[right fibration]], over an $\infty$-groupoid the notions of left/right fibrations and Kan fibrations coincide. This shows that the full [[sub-(∞,1)-category]] of $\infty Grpd/X$ on the right fibrations is equivalent to all of $\infty Grpd/X$.

\end{proof}
\hypertarget{for_general_fibered_categories}{}\subsection*{{For general fibered $(\infty,1)$-categories}}\label{for_general_fibered_categories}

The generalization of a [[fibered category]] to [[quasi-category]] theory is a [[Cartesian fibration|Cartesian]] [[fibrations of quasi-categories|fibration of quasi-categories]].

\begin{utheorem}
\textbf{($(\infty,1)$-Grothendieck construction)}

Let $C$ be an [[(∞,1)-category]]. There is an equivalence

\begin{displaymath}
Cart(C) \simeq Func(C^{op}, (\infty,1) Cat)
\end{displaymath}
where

\begin{itemize}%
\item on the left we have the $(\infty,1)$-category of [[Cartesian fibration]]s over $C$ -- incarnated as a [[sSet]]-[[subcategory]] of the [[overcategory]] $sSet/C$ on [[Cartesian fibration]]s;


\item and on the right the [[(∞,1)-category of (∞,1)-functors]] from $C^{op}$ to the [[(∞,1)-category of (∞,1)-categories]].



\end{itemize}
\end{utheorem}
In the next section we discuss how this statement is presented in terms of [[model categories]].

\hypertarget{ModCatCart}{}\subsubsection*{{Model category presentation}}\label{ModCatCart}

Regard the [[(∞,1)-category]] $C$ in its incarnation as a [[simplicially enriched category]].

Let $S$ be a [[simplicial set]], $\tau_{hc}(S)$ the corresponding [[simplicially enriched category]] (where $\tau_{hc}$ is the [[left adjoint]] of the [[homotopy coherent nerve]]) and let $\phi : \tau_{hc}(S) \to C$ be an [[sSet]]-[[enriched functor]].

\begin{udef}
\textbf{(extracting a marked simplicial presheaf from a marked fibration)} (HTT, section 3.2.1)

The \textbf{straightening functor}

\begin{displaymath}
St_\phi : sSet^+/S \to [C^{op}, sSet^+]
\end{displaymath}
from [[marked simplicial set]]s over $S$ to marked [[simplicial presheaves]] on $C^{op}$ is on the underlying simplicial sets (forgetting the marking) the same straightening functor as \hyperlink{GrpdModelCatVersion}{above}.

On the markings the functor acts as follows.

Each edge $f: d \rightarrow e$ of $X \in sSet/S$ gives rise to an edge $\tilde f \in St_\phi (X)(d) = K(\phi,p)(d,v)$: the [[join of simplicial sets|join]] 2-simplex $f \star v$ of $X^{\triangleright}$

\begin{displaymath}
\itexarray{                                                                   
    d && \stackrel{f}{\to} && e                                            
    \\                                                                     
    & {}_{\mathllap{\tilde d}}\searrow 
   & \stackrel{\tilde f}{\Rightarrow} 
   & \swarrow_{\mathrlap{\tilde e}}                                    
    \\                                                                     
    && v                                                                   
  }
\end{displaymath}
with image $\tilde f : \tilde d \to f^* \tilde e$ in the pushout $K(\phi,p)(d,v)=St_\phi X(d)$.

We define the straightening functor to assign that marking of edges which is the minimal one such that all such morphisms $\tilde f$ are marked in $St_\phi X(d)$, for all marked $f : d \to e$ in $X$: this means that this marking is being completed under the constraint that $St_\phi(X)$ be [[sSet]]-[[enriched functor|enriched functorial]].

For that, [[marked simplicial set|recall]] that the hom simplicial sets of $sSet^+$ are the spaces $Map^\sharp(X,Y)$, which consist of those simplices of the [[internal hom]] $Map(X,Y) := Y^X$ whose edges are all marked:

\begin{displaymath}
Map(X,Y)_n = Hom_{sSet^+}(X \times \Delta[n]^#, Y)
  \,.
\end{displaymath}
So we need to find a marking on the $St_\phi(X)(-)$ such that for all $g : \Delta[1] \to C(c,d)$ the composite

\begin{displaymath}
\Delta[1]
  \stackrel{g}{\to}
  C(c,d)
  \stackrel{St_\phi(X)(c,d)}{\to}
  Map(St_\phi(X)(d), St_\phi(X)(c))
\end{displaymath}
is a marked edge of the mapping complex. By the internal hom-adjunction this edge corresponds to a morphism

\begin{displaymath}
St_\phi(X)(g)
  :
  St_\phi(X)(d) \times \Delta[1] \rightarrow St_\phi(X)(c)
\end{displaymath}
and to be marked needs to carry edges of the form $\tilde f \times \{0 \to 1\}$ i.e. 1-cells $(\tilde f , Id) : \Delta[1] \to St_\phi(X)(d) \times \Delta[1]$ to marked edges

\begin{displaymath}
g^* \tilde f : \Delta[1] \stackrel{(\tilde f,Id)}{\to}
  St_\phi(X)(d)\times \Delta[1] \stackrel{St_\phi(X)(g)}{\to}
  St_{\phi}(X)(c)
\end{displaymath}
in $St_\phi(X)(c)$. So we need to ensure that the edges of this form are marked:

we define that the straightening functor marks an edge in $St_\phi(X)(c)$ iff it is of this form $g^* \tilde f$, for $f : d \to e$ a marked edge of $X$ and $g \in C(c,d)_1$.

As in the unmarked cae, the straightening functor has an [[sSet]]-[[right adjoint]], the \textbf{unstraightening functor}

\begin{displaymath}
n_\phi :  [C^{op}, sSet^+] \to sSet^+/S 
  \,.
\end{displaymath}
\end{udef}
This functor $Un_\phi$ exhibits the $(\infty,1)$-Grothendieck-construction proper, in that it constructs a [[Cartesian fibration]] from a given $(\infty,1)$-functor:

\begin{utheorem}
\textbf{(presentation of $(\infty,1)$-Grothendieck construction)}

This induces a [[Quillen adjunction]]

\begin{displaymath}
(St_\phi \dashv Un_\phi) : SSet^+/S
  \stackrel{\overset{Un_{\phi}}{\leftarrow}}{\underset{St_\phi}{\to}}
  [C^{op}, SSet^+]
\end{displaymath}
between the [[model structure for Cartesian fibrations]] and the projective [[global model structure on functors]] with values in the [[model structure on marked simplicial over-sets|model structure on marked simplicial sets]].

If $\phi$ is an equivalence in the [[model structure on simplicial categories]] then this Quillen adjunction is a [[Quillen equivalence]].

\end{utheorem}
\begin{proof}
This is [[Higher Topos Theory|HTT, theorem 3.2.0.1]].

\end{proof}
\hypertarget{OverCat}{}\paragraph*{{Over an ordinary category}}\label{OverCat}

In the case that $C$ happens to be an ordinary [[category]], the $(\infty,1)$-Grothendieck construction can be simplified and given more explicitly.

This is [[Higher Topos Theory|HTT, section 3.2.5]].

\begin{udef}
\textbf{(relative nerve functor)}

Let $C$ be a small category and let $f : C \to sSet$ be a functor. The simplicial set $N_f(C)$, the \textbf{relative nerve} of $C$ under $f$ is defined as follows:

an $n$-cell of $N_f(C)$ is

\begin{enumerate}%
\item a functor $\sigma : [n] \to C$;


\item for every $[k] \subset [n]$ a morphism $\tau(k) : \Delta[k] \to f(\sigma(k))$;


\item such that for all $[j] \subset [k] \subset [n]$ the diagram

\begin{displaymath}
\itexarray{
    \Delta[j] &\stackrel{\tau(j)}{\to}& f(\sigma(j))
    \\
    \downarrow && \downarrow^{\mathrlap{f(\sigma(j\to k))}}
    \\
    \Delta[k] &\stackrel{\tau(k)}{\to}& f(\sigma(k))
  }
\end{displaymath}
commutes.



\end{enumerate}
There is a canonical morphism

\begin{displaymath}
N_f(C) \to N(C)
\end{displaymath}
to the ordinary [[nerve]] of $C$, obtained by forgetting the $\tau$s.

\end{udef}
This is [[Higher Topos Theory|HTT, def. 3.2.5.2]].

\begin{uremark}
When $f$ is constant on the point, then $N_f(C) \to N(C)$ is an isomorphism of simplicial sets, so $N_f(C)$ this is the ordinary [[nerve]] of $C$.

The [[fiber]] of $N_f(C) \to N(C)$ over an object $c \in C$ is given by taking $\sigma$ to be constant on $C$. Then all the $\tau$s are fixed by the maximal $\tau(n) : \Delta[n] \to f(c)$. So the fiber of $N_f(C)$ over $c$ is $f(c)$.

\end{uremark}
\begin{udef}
\textbf{(marked relative nerve functor)}

Let $C$ be a small [[category]]. Define a functor

\begin{displaymath}
sSet^+/N(C) \leftarrow [C, sSet^+] : N^+
\end{displaymath}
by

\begin{displaymath}
(C \stackrel{F}{\to} sSet^+)
  \mapsto
  (N_f(C), E_F)
  \,,
\end{displaymath}
where $f : C^{op} \stackrel{F}{\to} sSet^+ \to sSet$ is $F$ with the marking forgotten, where $N_f(C)$ is the relative nerve of $C$ under $f$, and where the marking $E_F$ is given by \ldots{}

\end{udef}
This is [[Higher Topos Theory|HTT, def. 3.2.5.12]].

This functor has a [[left adjoint]] $\mathcal{F}^+$. The value of $\mathcal{F}^+(F)$ on some $c \in C$ is equivalent to the value of $St(F)$.

This is [[Higher Topos Theory|HTT, Lemma 3.2.5.17]].

\begin{uprop}
\textbf{($(\infty,1)$-Grothendieck construction over a category)}

The adjunction

\begin{displaymath}
(\mathcal{F}^+ \dashv N^+)
  : 
  sSet^+_{/N(C)} \stackrel{\overset{\mathcal{F}^+}{\to}}{\underset{N^+}{\leftarrow}}
  [C,sSet^+]
  \,.
\end{displaymath}
is a [[Quillen equivalence]] between the [[model structure for Cartesian fibrations|model structure for coCartesian fibrations]] and the projective [[global model structure on functors]].

\end{uprop}
\begin{proof}
This is [[Higher Topos Theory|HTT, prop. 3.2.5.18]].

\end{proof}
\hypertarget{relation_beween_the_model_structures}{}\subsubsection*{{Relation beween the model structures}}\label{relation_beween_the_model_structures}

\begin{utheorem}
Let $S$ be a [[simplicial set]].

There is a sequence of [[Quillen adjunction]]s

\begin{displaymath}
(sSet/S)_{Joyal}
  \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}}
  sSet^+/S
  \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}}
  (sSet^+/S)^{loc}
  \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}}
  (sSet/S)_{rfib}
  \stackrel{\overset{}{\to}}{\overset{}{\leftarrow}}
  (sSet/S)_{Quillen}
  \,.
\end{displaymath}
Where from left to right we have

\begin{enumerate}%
\item the [[model structure on an overcategory]] for the Joyal [[model structure for quasi-categories]];


\item the [[model structure for Cartesian fibrations]];


\item some localizaton of the model structure for Cartesian fibrations;


\item the [[model structure for right fibrations]]


\item the [[model structure on an overcategory]] for the Quillen [[model structure on simplicial sets]];



\end{enumerate}
The first and third Quillen adjunction here is a [[Quillen equivalence]] if $S$ is a [[Kan complex]].

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

\hypertarget{as_an_oplax_colimit}{}\subsubsection*{{As an (op)lax $\infty$-colimit}}\label{as_an_oplax_colimit}

The $(\infty,1)$-Grothendieck construction on an $\infty$-functor is equivalently its [[lax (infinity,1)-colimit]] (\hyperlink{GepnerHaugsengNikolaus15}{Gepner-Haugseng-Nikolaus 15}).

See also at \emph{[[Grothendieck construction]]} \emph{\href{Grothendieck%20construction#AsALaxColimit}{as a lax colimit}}.

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

\hypertarget{cartesian_fibrations_over_the_point}{}\subsubsection*{{Cartesian fibrations over the point}}\label{cartesian_fibrations_over_the_point}

For the base category $S$ being the point $S = {*}$, the $(\infty,1)$-Grothendieck construction naturally becomes essentially trivial. However, its model by the Quillen functor

\begin{displaymath}
St_\phi : sSet/* \simeq sSet \to [*,sSet] \simeq sSet
\end{displaymath}
is not entirely trivial and in fact produces a Quillen auto-equivalence of $sSet_{Quillen}$ with itself that plays a central role in the proof of the corresponding Quillen equivalence over general $S$.

\textbf{Definition}

Let $Q : \Delta \to sSet$ be the [[cosimplicial object|cosimplicial]] [[simplicial set]] given by

\begin{displaymath}
Q[n] := |J^n|(x,v)
  \,,
\end{displaymath}
where

\begin{displaymath}
J^n = C^{\triangleleft}(\Delta[n] \to \{x\})
  \,.
\end{displaymath}
Then: [[nerve and realization]] associated to $Q$ yield a [[Quillen equivalence]] of $sSet_{Quillen}$ with itself.

[[Higher Topos Theory|HTT, section 2.2.2]].

\ldots{}

\hypertarget{FibsOverInterval}{}\subsubsection*{{Cartesian fibrations over the interval}}\label{FibsOverInterval}

A [[Cartesian fibration]] $p : K \to \Delta[1]$ over the 1-[[simplex]] corresponds to a morphism $\Delta[1]^{op} \to$ [[(∞,1)Cat]], hence to an [[(∞,1)-functor]] $F : D \to C$.

By the above procedure we can express $F$ as the image of $p$ under the straightening functor. However, there is a more immediate way to extract this functor, which we now describe.

First recall the situation for the ordinary [[Grothendieck construction]]: given a [[Grothendieck fibration]] $K \to \{0 \to 1\}$, we obtain a functor $f : K_1 \to K_0$ between the fibers, by \emph{choosing} for each object $d \in K_1$ a [[Cartesian morphism]] $e_d \to d$. Then the universal property of Cartesian morphism yields for every morphism $d_1 \to d_2$ in $K_1$ the unique left vertical filler in

\begin{displaymath}
\itexarray{
    e_{d_1} &\to& d_1
    \\
    \downarrow && \downarrow
    \\
    e_{d_2} &\to& d_2
  }
  \,.
\end{displaymath}
And again by universality, this assignment is functorial: $K_1 \to K_0$.

Diagrammatically, the choice of Cartesian morphisms here is a lift $e$ in the diagram

\begin{displaymath}
\itexarray{
    K_1 &\hookrightarrow& K
    \\
    \downarrow &\nearrow_e& \downarrow
    \\
    K_1 \times \{0 \to 1\} &\to& \{0 \to 1\}
  }
  \,.
\end{displaymath}
This diagrammatic way of encoding the functor associated to a Grothendieck fibration over the interval generalizes straightforwardly to the [[quasi-category]] context.

\begin{udefn}
Given a [[Cartesian fibration]] $p : K \to \Delta[1]$ with fibers the [[quasi-categories]] $C := K_{0}$ and $D := K_{1}$, an \textbf{$(\infty,1)$-functor associated to the Cartesian fibration} $p$ is a functor $f : D \to C$ such that there exists a commuting diagram in [[sSet]]

\begin{displaymath}
\itexarray{
    D \times \Delta[1] &&\stackrel{F}{\to}&& K
    \\
    & \searrow && \swarrow_{\mathrlap{p}}
    \\
    && \Delta[1]
  }
\end{displaymath}
such that

\begin{itemize}%
\item $F|_{1} = Id_D$;


\item $F|_{0} = f$;


\item and for all $d \in D$, $F(\{d\}\times \{0  \to 1\})$ is a [[Cartesian morphism]] in $K$.



\end{itemize}
More generally, if we also specify possibly nontrivial [[equivalence of quasi-categories|equivalences of quasi-categories]] $h_0 : C \stackrel{\simeq}{\to} K_{0}$ and $h_1 : D \stackrel{\simeq}{\to} K_{1}$, then a functor is associated to $K$ and this choice of equivalences if the first twoo conditions above are generalized to

\begin{itemize}%
\item $F|_{1} = h_1$;


\item $F|_{0} = h_0 \circ f$;



\end{itemize}
\end{udefn}
This is [[Higher Topos Theory|HTT, def. 5.2.1.1]].

\begin{uprop}
For $p : K \to \Delta[1]$ a Cartesian fibration, the associated functor exists and is unique up to equivalence in the [[(∞,1)-category of (∞,1)-functors]] $Func(K_{0}, K_{1})$.

\end{uprop}
\begin{proof}
This is [[Higher Topos Theory|HTT, prop 5.2.1.5]].

Set $C := K_{0}$ and $D := K_{1}$.

With the notation described at [[model structure for Cartesian fibrations]], consider the commuting diagram

\begin{displaymath}
\itexarray{
    D^\flat \times \{1\} &\hookrightarrow& K^{\sharp}
    \\
    \downarrow && \downarrow^{\mathrlap{p}}
    \\
    D^{\flat} \times \Delta[1]^{#} &\to&
    \Delta[1]^#
  }
\end{displaymath}
in the category $sSet^+$ of marked simplicial sets.

Here the left vertical morphism is \href{http://ncatlab.org/nlab/show/model+structure+for+Cartesian+fibrations#MarkedAnodyne}{marked anodyne}: it is the [[smash product]] of the marked cofibration (monomorphism) $Id : D^\flat \to D^\flat$ with the marked anodyne morphism $\Delta[1]^# \to \Delta[0]$. By the stability properties discussed at \href{http://ncatlab.org/nlab/show/model+structure+for+Cartesian+fibrations#MarkedAnodyne}{Marked anodyne morphisms}, this implies that the morphism itself is marked anodyne.

As discussed there, this means that a lift $d : D^\flat \times \Delta[1]^# \to K^{\sharp}$ against the Cartesian fibration in

\begin{displaymath}
\itexarray{
    D^\flat \times \{1\} &\hookrightarrow& K^{\sharp}
    \\
    \downarrow &\nearrow_{s}& \downarrow^{\mathrlap{p}}
    \\
    D^{\flat} \times \Delta[1]^{#} &\to&
    \Delta[1]^#
  }
\end{displaymath}
exists. This exhibits an associated functor $f := s_0$.

Suppose now that another associated functor $f'$ is given. It will correspondingly come with its diagram

\begin{displaymath}
\itexarray{
    D^\flat \times \{1\} &\hookrightarrow& K^{\sharp}
    \\
    \downarrow &\nearrow_{s'}& \downarrow^{\mathrlap{p}}
    \\
    D^{\flat} \times \Delta[1]^{#} &\to&
    \Delta[1]^#
  }
  \,.
\end{displaymath}
Together this may be arranged to a diagram

\begin{displaymath}
\itexarray{
    D^\flat \times \Lambda[2]_2 
     &\stackrel{(s,s')}{\to}& K^{\sharp}
    \\
    \downarrow &\nearrow_{q}& \downarrow^{\mathrlap{p}}
    \\
    D^{\flat} \times \Delta[2]^{#} &\to&
    \Delta[1]^#
  }
  \,,
\end{displaymath}
where the top horizontal morphism picks the 2-[[horn]] in $K$ whose two edges are labeled by $s$ and $s'$, respectively.

Now, the left vertical morphism is still marked anodyne, and hence the lift $k$ exists, as indicated. Being a morphism of marked simplicial sets, it must map for each $d \in D$ the edge $\{d\}\times \{0\to 1\}$ to a [[Cartesian morphism]] in $K$, and due to the commutativity of the diagram this morphism must be in $K_0$, sitting over $\{0\}$. But as discussed there, a [[Cartesian morphism]] over a point is an equivalence. This means that the restriction

\begin{displaymath}
k|_{D \times \{0 \to 1\}} \to K_0
\end{displaymath}
is an invertible [[natural transformation]] between $f$ and $f'$, hence these are equivalent in the functor category.

\end{proof}
Conversely, every functor $f : D \to C$ gives rise to a Cartesian fibration that it is associated to, in the above sense.

\begin{uprop}
Every $(\infty,1)$-functor $f : D \to C$ is associated to some Cartesian fibration $p : K \to \Delta[1]$, and this is unique up to equivalence.

\end{uprop}
\begin{proof}
This is [[Higher Topos Theory|HTT, prop 5.2.1.3]].

The idea is that we obtain $K$ from first forming the cylinder $D \times \Delta[1]$ and the identifying the left boundary of that with $C$, using $f$.

Formally this means that we form the [[pushout]]

\begin{displaymath}
N := (D^\sharp \times \Delta[1]^#) \coprod_{D^\sharp \times \{0\}^#} C^\sharp
\end{displaymath}
in $sSet^+$, where $C^\sharp$ and $D^\sharp$ are $C$ and $D$ with precisely the [[equivalence in a quasi-category|equivalences]] marked. This comes canonically with a morphism

\begin{displaymath}
N \to \Delta[1]
\end{displaymath}
and does have the property that $N_0 = C$, $N_1 = D$ and that $f$ is associated to it in that the restriction of the canonical morphism $D \times \Delta[1] \to K$ to the 0-fiber is $f$. But it may fail to be a Cartesian fibration.

To fix this, use the [[small object argument]] to factor $N \to \Delta[1]$ as

\begin{displaymath}
N \to K \to \Delta[1]^#
  \,,
\end{displaymath}
where the first morphism is \href{http://ncatlab.org/nlab/show/model+structure+for+Cartesian+fibrations#MarkedAnodyne}{marked anodyne} and the second has the [[right lifting property]] with respect to all marked anodyne morphisms and is hence (since every morphism in $\Delta[1]^#$ is marked) a Cartesian fibration.

It then remains to check that $f$ is still associated to this $K \to \Delta[1]^#$. This is done by observing that in the small object argument $K$ is built succesively from [[pushout]]s of the form

\begin{displaymath}
\itexarray{
    A &\to& N_\alpha
    \\
    \downarrow && \downarrow & \searrow 
    \\
    B &\to& N_{\alpha+1} &\to& \Delta[1]
  }
  \,,
\end{displaymath}
where the morphisms on the left are the generators of marked anodyne morphisms (see \href{http://ncatlab.org/nlab/show/model+structure+for+Cartesian+fibrations#MarkedAnodyne}{here}). from this one checks that if the fiber $N_\alpha \times_{\Delta[1]} \{0\}$ is equivalent to $C$, then so is $N_{\alpha +1} \times_{\Delta[1]} \{0\}$ and similarly for $D$. By induction, it follows that $f$ is indeed associated to $K \to \Delta[1]$.

To see that the $K$ obtained this way is unique up to equivalence, consider\ldots{}

\end{proof}
\hypertarget{CartOverSimplex}{}\subsubsection*{{Cartesian fibrations over simplices}}\label{CartOverSimplex}

\ldots{} for the moment see [[Higher Topos Theory|HTT, section 3.2.2]] \ldots{}

\hypertarget{the_universal_cartesian_fibration}{}\subsubsection*{{The universal Cartesian fibration}}\label{the_universal_cartesian_fibration}

for the moment see

\begin{itemize}%
\item [[universal fibration of (∞,1)-categories]].

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

\begin{itemize}%
\item [[operadic (∞,1)-Grothendieck construction]]


\item [[Grothendieck construction for model categories]]



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

The construction for $\infty$-groupoid fibrations i.e. left/right fibrations is the content of section 2.2.1, that of quasi-category fibrations i.e. Cartesian fibrations that

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

\end{itemize}
More on model-category theoretic construction of the $\infty$-Grothendieck construction with values in $\infty$-groupoids is in

\begin{itemize}%
\item [[Gijs Heuts]], [[Ieke Moerdijk]], \emph{Left fibrations and homotopy colimits} (\href{http://arxiv.org/abs/1308.0704}{arXiv:1308.0704})

\end{itemize}
Discussion in terms of [[lax (infinity,1)-colimits]] is in

\begin{itemize}%
\item [[David Gepner]], [[Rune Haugseng]], [[Thomas Nikolaus]], \emph{Lax colimits and free fibrations in $\infty$-categories} (\href{http://arxiv.org/abs/1501.02161}{arXiv:1501.02161})

\end{itemize}
[[!redirects (∞,1)-Grothendieck construction]]



\end{document}