\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*{(∞,1)-limit} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{category_theory}{}\paragraph*{{$(\infty,1)$-Category theory}}\label{category_theory} [[!include quasi-category theory contents]] \hypertarget{limits_and_colimits}{}\paragraph*{{Limits and colimits}}\label{limits_and_colimits} [[!include infinity-limits - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{InTermsOfSlices}{In terms of slice $\infty$-categories}\dotfill \pageref*{InTermsOfSlices} \linebreak \noindent\hyperlink{in_terms_of_hom_adjunction}{In terms of $\infty$-Hom adjunction}\dotfill \pageref*{in_terms_of_hom_adjunction} \linebreak \noindent\hyperlink{in_terms_of_products_and_equalizers}{In terms of products and equalizers}\dotfill \pageref*{in_terms_of_products_and_equalizers} \linebreak \noindent\hyperlink{TermsOfHomotopy}{In terms of homotopy limits}\dotfill \pageref*{TermsOfHomotopy} \linebreak \noindent\hyperlink{CommutativityOfLimits}{Commutativity of limits}\dotfill \pageref*{CommutativityOfLimits} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{limits_of_special_shape}{$\infty$-Limits of special shape}\dotfill \pageref*{limits_of_special_shape} \linebreak \noindent\hyperlink{coproduct}{Coproduct}\dotfill \pageref*{coproduct} \linebreak \noindent\hyperlink{pullback__pushout}{Pullback / Pushout}\dotfill \pageref*{pullback__pushout} \linebreak \noindent\hyperlink{PushoutPasting}{Pasting law of pushouts}\dotfill \pageref*{PushoutPasting} \linebreak \noindent\hyperlink{coequalizer}{Coequalizer}\dotfill \pageref*{coequalizer} \linebreak \noindent\hyperlink{quotients}{Quotients}\dotfill \pageref*{quotients} \linebreak \noindent\hyperlink{Tensoring}{Tensoring and cotensoring with an $\infty$-groupoid}\dotfill \pageref*{Tensoring} \linebreak \noindent\hyperlink{recap_of_the_1categorical_situation}{Recap of the 1-categorical situation}\dotfill \pageref*{recap_of_the_1categorical_situation} \linebreak \noindent\hyperlink{definition_3}{Definition}\dotfill \pageref*{definition_3} \linebreak \noindent\hyperlink{ModelsForTensoring}{Models}\dotfill \pageref*{ModelsForTensoring} \linebreak \noindent\hyperlink{InOvercategories}{Limits in over-$(\infty,1)$-categories}\dotfill \pageref*{InOvercategories} \linebreak \noindent\hyperlink{WithValInooGrpd}{Limits and colimits with values in $\infty Grpd$}\dotfill \pageref*{WithValInooGrpd} \linebreak \noindent\hyperlink{ColimitsInInfinityCat}{Limits and colimits with values in $(\infty,1)$Cat}\dotfill \pageref*{ColimitsInInfinityCat} \linebreak \noindent\hyperlink{limits_in_functor_categories}{Limits in $\infty$-functor categories}\dotfill \pageref*{limits_in_functor_categories} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak \noindent\hyperlink{in_homotopy_type_theory}{In homotopy type theory}\dotfill \pageref*{in_homotopy_type_theory} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} The notion of [[limit]] and [[colimit]] generalize from [[category theory]] to [[(∞,1)-category theory]]. One model for [[(∞,1)-categories]] are [[quasi-categories]]. This entry discusses limits and colimits in quasi-categories. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} \begin{defn} \label{}\hypertarget{}{} For $K$ and $C$ two [[quasi-category|quasi-categories]] and $F : K \to C$ an [[(∞,1)-functor]] (a morphism of the underlying [[simplicial set]]s) , the \textbf{limit} over $F$ is, if it exists, the [[terminal object in a quasi-category|quasi-categorical terminal object]] in the [[over quasi-category]] $C_{/F}$: \begin{displaymath} \underset{\leftarrow}{\lim} F \coloneqq TerminalObj(C_{/F}) \end{displaymath} (well defined up to a contractible space of choices). A \textbf{colimit} in a quasi-category is accordingly a limit in the [[opposite quasi-category]]. \end{defn} \begin{remark} \label{}\hypertarget{}{} Notice from the discussion at [[join of quasi-categories]] that there are two definitions -- denoted $\star$ and $\diamondsuit$ -- of join, which yield results that differ as simplicial sets, though are equivalent as quasi-categories. The notation $C_{/F}$ denotes the definition of [[over quasi-category]] induced from $\star$, while the notation $C^{/F}$ denotes that induced from $\diamondsuit$. Either can be used for the computation of limits in a quasi-category, as for quasi-categorical purposes they are weakly equivalent. So we also have \begin{displaymath} \underset{\leftarrow}{\lim} F \coloneqq TerminalObj(C^{/F}) \,. \end{displaymath} See [[Higher Topos Theory|HTT, prop 4.2.1.5]]. \end{remark} \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{InTermsOfSlices}{}\subsubsection*{{In terms of slice $\infty$-categories}}\label{InTermsOfSlices} \begin{prop} \label{}\hypertarget{}{} Let $\mathcal{C}$ be a [[quasi-category]] and let $f \colon K \to \mathcal{C}$ be a [[diagram]] with $(\infty,1)$-colimiting [[cocone]] $\tilde f \colon K \star \Delta^0 \to \mathcal{C}$. Then the induced map of [[slice (∞,1)-categories|slice quasi-categories]] \begin{displaymath} \mathcal{C}_{/\tilde f} \to \mathcal{C}_{f} \end{displaymath} is an [[acyclic Kan fibration]]. \end{prop} \begin{prop} \label{SlicingOverLimitingCone}\hypertarget{SlicingOverLimitingCone}{} For $F \colon \mathcal{K} \to \mathcal{C}$ a diagram in an $(\infty,1)$-category and $\underset{\leftarrow}{\lim} F$ its limit, there is a natural [[equivalence of (∞,1)-categories]] \begin{displaymath} \mathcal{C}_{/F} \simeq \mathcal{C}_{/\underset{\leftarrow}{\lim} F} \end{displaymath} between the [[slice (∞,1)-categories]] over $F$ (the $(\infty,1)$-category of $\infty$-[[cones]] over $F$) and over just $\underset{\leftarrow}{\lim}F$. \end{prop} \begin{proof} Let $\tilde F \colon \Delta^0 \star \mathcal{K} \to \mathcal{C}$ be the limiting cone. The canonical cospan of $\infty$-functors \begin{displaymath} \ast \to \Delta^0 \star \mathcal{K} \leftarrow \mathcal{K} \end{displaymath} induces a span of slice $\infty$-categories \begin{displaymath} \mathcal{C}_{/\underset{\leftarrow}{\lim}F} \leftarrow \mathcal{C}_{/\tilde F} \rightarrow \mathcal{C}_{/F} \,. \end{displaymath} The right functor is an equivalence by prop. \ref{SlicingOverLimitingCone}. The left functor is induced by restriction along an op-[[final (∞,1)-functor]] (by the Examples discussed there) and hence is an equivalence by the discussion at \emph{[[slice (∞,1)-category]]} (\hyperlink{Lurie}{Lurie, prop. 4.1.1.8}). \end{proof} This appears for instance in (\hyperlink{Lurie}{Lurie, proof of prop. 1.2.13.8}). \hypertarget{in_terms_of_hom_adjunction}{}\subsubsection*{{In terms of $\infty$-Hom adjunction}}\label{in_terms_of_hom_adjunction} The definition of the limit in a quasi-category in terms of terminal objects in the corresponding [[over quasi-category]] is well adapted to the particular nature the incarnation of $(\infty,1)$-categories by quasi-categories. But more intrinsically in $(\infty,1)$-category theory, it should be true that there is an [[adjunction]] characterization of $(\infty,1)$-limits : limit and colimit, should be (pointwise or global) [[right adjoint|right]] and [[left adjoint|left]] [[adjoint (infinity,1)-functor]] of the constant diagram $(\infinity,1)$-functor, $const : K \to Func(K,C)$. \begin{displaymath} (colim \dashv const \dashv lim) : Func(K,C) \stackrel{\overset{lim}{\to}}{\stackrel{\overset{const}{\leftarrow}} {\underset{colim}{\to}}} Func(*,C) \simeq C \,. \end{displaymath} By the discussion at [[adjoint (∞,1)-functor]] ([[Higher Topos Theory|HTT, prop. 5.2.2.8]]) this requires exhibiitng a morphism $\eta : Id_{Func(K,C)} \to const colim$ in $Func(Func(K,C),Func(K,C))$ such that for every $f \in Func(K,C)$ and $Y \in C$ the induced morphism \begin{displaymath} Hom_{C}(colim(f),Y) \to Hom_{Func(K,C)}(const colim(f), const Y) \stackrel{Hom(\eta, const Y)}{\to} Hom_{Func(K,Y)}(f, const Y) \end{displaymath} is a weak equivalence in $sSet_{Quillen}$. But first consider the following pointwise characterization. \begin{prop} \label{}\hypertarget{}{} Let $C$ be a [[quasi-category]], $K$ a [[simplicial set]]. A [[co-cone]] [[diagram]] $\bar p : K \star \Delta[0] \to C$ with cone point $X \in C$ is a [[colimit|colimiting]] [[diagram]] (an initial object in $C_{p/}$) precisely if for every object $Y \in C$ the morphism \begin{displaymath} \phi_Y : Hom_C(X,Y) \to Hom_{Func(K,C)}(p, const Y) \end{displaymath} induced by the morpism $p \to const X$ that is encoded by $\bar p$ is an equivalence (i.e. a [[homotopy equivalence]] of [[Kan complex]]es). \end{prop} \begin{proof} This is [[Higher Topos Theory|HTT, lemma 4.2.4.3]]. The key step is to realize that $Hom_{Func(K,C)}(p, const Y)$ is given (up to equivalence) by the [[pullback]] $C^{p/} \times_C \{Y\}$ in [[sSet]]. Here is a detailed way to see this, using the discussion at [[hom-object in a quasi-category]]. We have that $Hom_{Func(K,C)}(p, const Y)$ is given by $(C^K)^{p/} \times_{C^K} const Y$. We compute \begin{displaymath} \begin{aligned} ((C^K)^{p/} \times_{C^K} const Y)_n & = Hom_{{\Delta[0]}/sSet}( \Delta[0] \diamondsuit \Delta[n] , C^K ) \times_{(C^K)_n} \{const Y\} \\ & = Hom_{{\Delta[0]}/sSet}( \Delta[0] \coprod_{\Delta[n]} \Delta[n] \times \Delta[1] , C^K ) \times_{(C^K)_n} \{const Y\} \\ & = \{p\} \times_{Hom(\Delta[0],C^K)} Hom(\Delta[0], C^K) \times_{Hom(\Delta[n], C^K)} Hom(\Delta[n] \times \Delta[1], C^K) \times_{Hom(\Delta[n], C^K)} \{const Y\} \\ & = \{p\} \times_{Hom(K,C)} Hom(K,C) \times_{Hom(\Delta[n]\times K,C)} Hom(\Delta[n]\times K \times \Delta[1], C) \times_{Hom(\Delta[n]\times K, C)} Hom(\Delta[n],C) \times_{\Delta[n],C} \{Y\} \\ &= \{p\} \times_{Hom(K,C)} Hom(K \diamondsuit \Delta[n], C) \times_{Hom(\Delta[n],C)} \{Y\} \\ &= (C^{p/}\times_C \{Y\})_n \end{aligned} \end{displaymath} Under this identification, $\phi_Y$ is the morphism \begin{displaymath} \left( C^{X/} \stackrel{\phi'}{\to} C^{\bar p/} \stackrel{\phi''}{\to} C^{p/} \right) \times_C \{Y\} \,, \end{displaymath} in [[sSet]] where $\phi'$ is a section of the map $C^{\bar p/} \to C^{X/}$, (which one checks is an acyclic [[Kan fibration]]) obtained by choosing composites of the co-cone components with a given morphism $X \to Y$. The morphism $\phi''$ is a [[left fibration]] (using [[Higher Topos Theory|HTT, prop. 4.2.1.6]]) One finds that the morphism $\phi''$ is a [[left fibration]]. The strategy for the completion of the proof is: realize that the first condition of the proposition is equivalent to $\phi''$ being an acyclic Kan fibration, and the second statement equivalent to $\phi''_Y$ being an acyclic Kan fibration, then show that these two conditions in turn are equivalent. \end{proof} \hypertarget{in_terms_of_products_and_equalizers}{}\subsubsection*{{In terms of products and equalizers}}\label{in_terms_of_products_and_equalizers} A central theorem in ordinary [[category theory]] asserts that a [[category]] has [[limit]]s already if it has [[product]]s and [[equalizer]]s. The analog statement is true here: \begin{prop} \label{}\hypertarget{}{} Let $\kappa$ be a [[regular cardinal]]. An [[(∞,1)-category]] $C$ has all $\kappa$-small limits precisely if it has [[equalizer]]s and $\kappa$-small [[product]]s. \end{prop} This is [[Higher Topos Theory|HTT, prop. 4.4.3.2]]. \hypertarget{TermsOfHomotopy}{}\subsubsection*{{In terms of homotopy limits}}\label{TermsOfHomotopy} The notion of [[homotopy limit]], which exists for [[model categories]] and in particular for [[simplicial model categories]] and in fact in all plain [[Kan complex]]-[[enriched categories]] -- as described in more detail at [[homotopy Kan extension]] -- is supposed to be a model for $(\infty,1)$-categorical limits. In particular, under sending the Kan-complex enriched categories $C$ to quasi-categories $N(C)$ using the [[homotopy coherent nerve]] functor, homotopy limits should precisely corespond to quasi-categorical limits. That this is indeed the case is asserted by the following statements. \begin{prop} \label{}\hypertarget{}{} Let $C$ and $J$ be [[Kan complex]]-[[enriched categories]] and let $F : J \to C$ be an [[sSet]]-[[enriched functor]]. Then a [[cocone]] $\{\eta_i : F(i) \to c\}_{i \in J}$ under $F$ exhibits the object $c \in C$ as a [[homotopy colimit]] (in the sense discussed in detail at [[homotopy Kan extension]]) precisely if the induced morphism of quasi-categories \begin{displaymath} \bar {N(F)} : N(J)^{\triangleright} \to N(C) \end{displaymath} is a quasi-categorical colimit [[diagram]] in $N(C)$. \end{prop} Here $N$ is the [[homotopy coherent nerve]], $N(J)^{\triangleright}$ the [[join of quasi-categories]] with the point, $N(F)$ the image of the simplicial functor $F$ under the homotopy coherent nerve and $\bar{N(F)}$ its extension to the join determined by the cocone maps $\eta$. \begin{proof} This is [[Higher Topos Theory|HTT, theorem 4.2.4.1]] A central ingredient in the proof is the fact, discused at [[(∞,1)-category of (∞,1)-functors]] and at [[model structure on functors]], that [[sSet]]-[[enriched functor]]s do model [[(∞,1)-functor]]s, in that for $A$ a [[combinatorial simplicial model category]], $S$ a [[quasi-category]] and $\tau(S)$ the corresponding $sSet$-category under the left adjoint of the [[homotopy coherent nerve]], we have an [[equivalence of quasi-categories]] \begin{displaymath} N(([C,A]_{proj})^\circ) \simeq Func(S, N(A^\circ)) \end{displaymath} and the same is trued for $A$ itself replaced by a [[chunk of a model category|chunk]] $U \subset A$. With this and the discussion at [[homotopy Kan extension]], we find that the cocone components $\eta$ induce for each $a \in [C,sSet]$ a [[homotopy equivalence]] \begin{displaymath} C(c,a) \stackrel{}{\to} [J^{op}, C](j F, const a) \end{displaymath} which is hence equivalently an equivalence of the corresponding [[hom-object in a quasi-category|quasi-categorical hom-objects]]. The claim follows then from the above discussion of characterization of (co)limits in terms of $\infty$-hom adjunctions. \end{proof} \begin{cor} \label{}\hypertarget{}{} The quasi-category $N(A^\circ)$ [[presentable (∞,1)-category|presented]] by a [[combinatorial simplicial model category]] $A$ has all small quasi-categorical limits and colimits. \end{cor} \begin{proof} This is [[Higher Topos Theory|HTT, 4.2.4.8]]. It follows from the fact that $A$ has (pretty much by definition of [[model category]] and [[combinatorial model category]]) all [[homotopy limit]]s and [[homotopy colimit]]s (in fact all [[homotopy Kan extension]]s) by the above proposition. \end{proof} Since $(\infty,1)$-categories equivalent to those of the form $N(A^\circ)$ for $A$ a [[combinatorial simplicial model category]] are precisely the [[locally presentable (∞,1)-categories]], it follows from this in particular that every locally presentable $(\infty,1)$-category has all limits and colimits. \hypertarget{CommutativityOfLimits}{}\subsubsection*{{Commutativity of limits}}\label{CommutativityOfLimits} The following proposition says that if for an $(\infty,1)$-functor $F : X \times Y \to C$ limits (colimits) over each of the two variables exist separately, then they commute. \begin{prop} \label{}\hypertarget{}{} Let $X$ and $Y$ be [[simplicial set]]s and $C$ a [[quasi-category]]. Let $p : X^{\triangleleft} \times Y^{\triangleleft} \to C$ be a [[diagram]]. If \begin{enumerate}% \item for every object $x \in X^{\triangleleft}$ (including the cone point) the restricted diagram $p_x : Y^{\triangleleft} \to C$ is a limit diagram; \item for every object $y \in Y$ (not including the cone point) the restricted diagram $p_y : X^{\triangleleft} \to C$ is a limit diagram; \end{enumerate} then, with $c$ denoting the cone point of $Y^{\triangleleft}$, the restricted diagram, $p_c : X^{\triangleleft} \to C$ is also a limit diagram. \end{prop} \begin{proof} This is [[Higher Topos Theory|HTT, lemma 5.5.2.3]] \end{proof} In other words, suppose that $\lim_x F(x,y)$ exists for all $y$ and $\lim_y F(x,y)$ exists for all $x$ and also that $\lim_y (\lim_x F(x,y))$ exists, then this object is also $\lim_x \lim_y F(x,y)$. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{limits_of_special_shape}{}\subsubsection*{{$\infty$-Limits of special shape}}\label{limits_of_special_shape} \hypertarget{coproduct}{}\paragraph*{{Coproduct}}\label{coproduct} \ldots{} \hypertarget{pullback__pushout}{}\paragraph*{{Pullback / Pushout}}\label{pullback__pushout} See also [[(∞,1)-pullback]]. The non-degenerate cells of the [[simplicial set]] $\Delta[1] \times \Delta[1]$ obtained as the [[cartesian product]] of the simplicial 1-[[simplex]] with itself look like \begin{displaymath} \itexarray{ (0,0) &\to& (1,0) \\ \downarrow &\searrow& \downarrow \\ (0,1) &\to& (1,1) } \end{displaymath} A \textbf{sqare} in a [[quasi-category]] $C$ is an image of this in $C$, i.e. a morphism \begin{displaymath} s : \Delta[1] \times \Delta[1] \to C \,. \end{displaymath} The simplicial square $\Delta[1]^{\times 2}$ is [[isomorphism|isomorphic]], as a [[simplicial set]], to the [[join of simplicial sets]] of a 2-[[horn]] with the point: \begin{displaymath} \Delta[1] \times \Delta[1] \simeq \{v\} \star \Lambda[2]_2 = \left( \itexarray{ v &\to& 1 \\ \downarrow &\searrow& \downarrow \\ 0 &\to& 2 } \right) \end{displaymath} and \begin{displaymath} \Delta[1] \times \Delta[1] \simeq \Lambda[2]_0 \star \{v\} = \left( \itexarray{ 0&\to& 1 \\ \downarrow &\searrow& \downarrow \\ 2 &\to& v } \right) \,. \end{displaymath} If a square $\Delta[1] \times \Delta[1] \simeq \Lambda[2]_0 \star \{v\} \to C$ exhibits $\{v\} \to C$ as a colimit over $F : \Lambda[2]_0 \to C$, we say the colimit \begin{displaymath} v := \lim_\to F := F(1) \coprod_{F(0)} F(2) \end{displaymath} is [[generalized the|the]] \textbf{pushout} of the diagram $F$. \hypertarget{PushoutPasting}{}\paragraph*{{Pasting law of pushouts}}\label{PushoutPasting} We have the following $(\infty,1)$-categorical analog of the familiar \href{http://ncatlab.org/nlab/show/pullback#Pasting}{pasting law of pushouts} in ordinary [[category theory]]: \begin{prop} \label{}\hypertarget{}{} A pasting diagram of two squares is a morphism \begin{displaymath} \Delta[2] \times \Delta[1] \to C \,. \end{displaymath} Schematically this looks like \begin{displaymath} \itexarray{ x &\to& y &\to& z \\ \downarrow && \downarrow && \downarrow \\ x' &\to& y' &\to& z' } \,. \end{displaymath} If the left square is a pushout diagram in $C$, then the right square is precisely if the outer square is. \end{prop} \begin{proof} A proof appears as [[Higher Topos Theory|HTT, lemma 4.4.2.1]] \end{proof} \hypertarget{coequalizer}{}\paragraph*{{Coequalizer}}\label{coequalizer} \ldots{} \hypertarget{quotients}{}\paragraph*{{Quotients}}\label{quotients} \begin{itemize}% \item [[infinity-quotient]] \end{itemize} \hypertarget{Tensoring}{}\paragraph*{{Tensoring and cotensoring with an $\infty$-groupoid}}\label{Tensoring} \hypertarget{recap_of_the_1categorical_situation}{}\paragraph*{{Recap of the 1-categorical situation}}\label{recap_of_the_1categorical_situation} An ordinary [[category]] with [[limit]]s is canonically [[power|cotensored]] over [[Set]]: For $S, T \in$ [[Set]] and $const_T : S \to Set$ the [[diagram]] parameterized by $S$ that is constant on $T$, we have \begin{displaymath} \lim_{\leftarrow} const_T \simeq T^S \,. \end{displaymath} Accordingly the cotensoring \begin{displaymath} (-)^{(-)} : Set^{op} \times C \to C \end{displaymath} is defined by \begin{displaymath} c^S := \lim_{\leftarrow} (S \stackrel{const_c}{\to} C) = \prod_{S} c \,. \end{displaymath} And by continuity of the [[hom-functor]] this implies the required natural isomorphisms \begin{displaymath} Hom_C(d,c^S) = Hom_C(d, {\lim_{\leftarrow}}_S c) \simeq {\lim_{\leftarrow}}_S Hom_C(d,c) \simeq Set(S,Hom_C(d,C)) \,. \end{displaymath} Correspondingly if $C$ has [[colimit]]s, then the [[copower|tensoring]] \begin{displaymath} (-) \otimes (-) : Set \times C \to C \end{displaymath} is given by forming [[colimit]]s over constant diagrams: $S \otimes c := {\lim_{\to}}_S c$, and again by continuity of the [[hom-functor]] we have the required natural isomorphism \begin{displaymath} Hom_C(S \otimes c, d) = Hom_C({\lim_{\to}}_S c,d) \simeq {\lim_{\leftarrow}}_S Hom_C(c,d) \simeq Set(S,Hom_C(c,d)) \,. \end{displaymath} Of course all the colimits appearing here are just [[coproduct]]s and all limits just [[product]]s, but for the generalization to $(\infty,1)$-categories this is a misleading simplification, it is really the notion of limit and colimit that matters here. \hypertarget{definition_3}{}\paragraph*{{Definition}}\label{definition_3} We expect for $S, T \in$ [[∞Grpd]] and for $const_T : S \to \infty Grpd$ the constant diagram, that \begin{displaymath} \lim_{\leftarrow} const_T \simeq T^S \,, \end{displaymath} where on the right we have the [[internal hom]] of $\infty$-groupoids, which is modeled in the [[model structure on simplicial sets]] $sSet_{Quillen}$ by the fact that this is a [[closed monoidal category|closed]] [[monoidal category]]. Correspondingly, for $C$ an $(\infty,1)$-category with colimits, it is [[copower|tensored]] over [[∞Grpd]] by setting \begin{displaymath} (-)\otimes (-) : \infty Grpd \times C \to C \end{displaymath} \begin{displaymath} S \otimes c := {\lim_{\to}}_S c \,, \end{displaymath} where now on the right we have the $(\infty,1)$-categorical colimit over the constant diagram $const : S \to C$ of shape $S$ on $c$. Then by the $(\infty,1)$-continuity of the hom, and using the above characterization of the [[internal hom]] in $\infty Grpd$ we have the required natural equivalence \begin{displaymath} Hom_C(S \otimes c, d) = Hom_C({\lim_{\to}}_S c, d) \simeq {\lim_{\leftarrow}}_S Hom_C(c,d) \simeq \infty Grpd(S,Hom_C(c,d)) \,. \end{displaymath} The following proposition should assert that this is all true \begin{prop} \label{TensoringProposition}\hypertarget{TensoringProposition}{} The $(\infty,1)$-categorical colimit ${\lim_{\to}} c$ over the diagram of shape $S \in \infty Grpd$ constant on $c \in C$ is characterized by the fact that it induces natural equivalences \begin{displaymath} Hom_C({\lim_{\to}}_S c, d) \simeq \infty Grpd(S, Hom_C(c,d)) \end{displaymath} for all $d \in C$. \end{prop} This is essentially [[Higher Topos Theory|HTT, corollary 4.4.4.9]]. \begin{cor} \label{EveryInfinityGroupoidIsHomotopyColimitOfConstantFunctorOverItself}\hypertarget{EveryInfinityGroupoidIsHomotopyColimitOfConstantFunctorOverItself}{} Every [[∞-groupoid]] $S$ is the $(\infty,1)$-colimit in [[∞Grpd]] of the constant diagram on the [[point]] over itself: \begin{displaymath} S \simeq {\lim_{\to}}_S const_* \,. \end{displaymath} \end{cor} This justifies the following definition \begin{defn} \label{}\hypertarget{}{} For $C$ an $(\infty,1)$-category with colimits, the \textbf{tensoring of $C$ over $\infty Grpd$} is the $(\infty,1)$-functor \begin{displaymath} (-) \otimes (-) : \infty Grpd \times C \to C \end{displaymath} given by \begin{displaymath} S \otimes c = \lim_{\to} (const_c : S \to C) \,. \end{displaymath} \end{defn} See [[Higher Topos Theory|HTT, section 4.4.4]]. \hypertarget{ModelsForTensoring}{}\paragraph*{{Models}}\label{ModelsForTensoring} We discuss models for $(\infty,1)$-(co)limits in terms of ordinary [[category theory]] and [[homotopy theory]]. \begin{lemma} \label{}\hypertarget{}{} If $C$ is [[presentable (infinity,1)-category|presented]] by a [[simplicial model category]] $A$, in that $C \simeq A^\circ$, then the $(\infty,1)$-tensoring and $(\infty,1)$-cotensoring of $C$ over [[∞Grpd]] is modeled by the ordinary [[copower|tensoring]] and [[power|powering]] of $A$ over [[sSet]]: For $\hat c \in A$ cofibant and representing an object $c \in C$ and for $S \in sSet$ any simplicial set, we have an equivalence \begin{displaymath} c \otimes S \simeq \hat C \cdot S \,. \end{displaymath} \end{lemma} \begin{proof} The powering in $A$ satisfies the [[natural isomorphism]] \begin{displaymath} sSet(S,A(\hat c,\hat d)) \simeq A(\hat c \cdot S, \hat d) \end{displaymath} in [[sSet]]. For $\hat c$ a cofibrant and $\hat d$ a fibrant representative, we have that both sides here are [[Kan complex]]es that are equivalent to the corresponding [[derived hom space]]s in the corresponding $(\infty,1)$-category $C$, so that this translates into an equivalence \begin{displaymath} Hom_C(c \cdot S, d) \simeq \infty Grpd(S, Hom_C(c,d)) \,. \end{displaymath} The claim then follows from the above proposition. \end{proof} \hypertarget{InOvercategories}{}\subsubsection*{{Limits in over-$(\infty,1)$-categories}}\label{InOvercategories} \begin{prop} \label{}\hypertarget{}{} For $C$ an $(\infty,1)$-category, $X : D \to C$ a diagram, $C/X$ the [[over-(∞,1)-category]] and $F : K \to C/X$ a diagram in the over-$(\infty,1)$-category, then the [[(∞,1)-limit]] $\lim_{\leftarrow} F$ in $C/X$ coincides with the $(\infty,1)$-limit $\lim_{\leftarrow} F/X$ in $C$. \end{prop} \begin{proof} Modelling $C$ as a [[quasi-category]] we have that $C/X$ is given by the [[simplicial set]] \begin{displaymath} C/X : [n] \mapsto Hom_X([n] \star D, C) \,, \end{displaymath} where $\star$ denotes the [[join of simplicial sets]]. The limit $\lim_{\leftarrow} F$ is the initial object in $(C/X)/F$, which is the quasi-category given by the simplicial set \begin{displaymath} (C/X)/F : [n] \mapsto Hom_{F}( [n] \star K, C/X) \,. \end{displaymath} Since the join preserves colimits of simplicial sets in both arguments, we can apply the [[co-Yoneda lemma]] to decompose $[n] \star K = {\lim_{\underset{{[r] \to [n]\star K}}{\to}}} [r]$, use that the [[hom-functor]] sends colimits in the first argument to limits and obtain \begin{displaymath} \begin{aligned} Hom([n] \star K, C/X) &\simeq Hom( {\lim_{\to}}_r [r], C/X) \\ & \simeq {\lim_{\leftarrow}}_r Hom([r], C/X) \\ & \simeq {\lim_{\leftarrow}}_r Hom_F( [r] \star D, C ) \\ & \simeq Hom_F({\lim_{\to}}_r ([r] \star D), C ) \\ & \simeq Hom_F( ({\lim_{\to}}_r[r]) \star D, C ) \\ & \simeq Hom_F(([n] \star K) \star D, C) \\ & \simeq Hom_F([n] \star (K \star D), C) \end{aligned} \,. \end{displaymath} Here $Hom_F([r]\star D,C)$ is shorthand for the hom in the (ordinary) [[under category]] $sSet^{D/}$ from the canonical inclusion $D \to [r] \star D$ to $X : D \to C$. Notice that we use the 1-categorical analog of the statement that we are proving here when computing the colimit in this under-category as just the colimit in $sSet$. We also use that the [[join of simplicial sets]], being given by [[Day convolution]] is an associative tensor product. In conclusion we have an isomorphism of simplicial sets \begin{displaymath} (C/X)/F \simeq C/(X/F) \end{displaymath} and therefore the initial objects of these quasi-categories coincide on both sides. This shows that $\lim_{\leftarrow} F$ is computed as an initial object in $C/(X/F)$. \end{proof} \hypertarget{WithValInooGrpd}{}\subsubsection*{{Limits and colimits with values in $\infty Grpd$}}\label{WithValInooGrpd} Limits and colimits over a [[(∞,1)-functor]] with values in the [[(∞,1)-category]] [[∞-Grpd]] of [[∞-groupoids]] may be reformulated in terms of the [[universal fibration of (∞,1)-categories]], hence in terms of the [[(∞,1)-Grothendieck construction]]. Let [[∞Grpd]] be the [[(∞,1)-category]] of [[∞-groupoid]]s. Let the [[(∞,1)-functor]] $Z|_{Grpd} \to \infty Grpd^{op}$ be the [[universal fibration of (infinity,1)-categories|universal ∞-groupoid fibration]] whose fiber over the object denoting some $\infty$-groupoid is that very $\infty$-groupoid. Then let $X$ be any [[∞-groupoid]] and \begin{displaymath} F : X \to \infty Grpd \end{displaymath} an [[(∞,1)-functor]]. Recall that the [[Cartesian fibration|coCartesian fibration]] $E_F \to X$ classified by $F$ is the pullback of the [[universal fibration of ∞-groupoids]] $Z|_{Grpd}$ along F: \begin{displaymath} \itexarray{ E_F &\to& Z|_{Grpd} \\ \downarrow && \downarrow \\ X &\stackrel{F}{\to}& \infty Grpd } \end{displaymath} \begin{prop} \label{InfinityGroupoidalCoLimitsViaIntegrationAndSlicing}\hypertarget{InfinityGroupoidalCoLimitsViaIntegrationAndSlicing}{} Let the assumptions be as above. Then: \begin{itemize}% \item The $\infty$-colimit of $F$ is equivalent to the [[(∞,1)-Grothendieck construction]] $E_F$: \begin{displaymath} \underset{\longrightarrow}{\lim} F \simeq E_F \end{displaymath} \item The $\infty$-limit of $F$ is equivalent to the [[∞-groupoid of sections]] of $E_F \to X$ \begin{displaymath} \underset{\longleftarrow}{\lim} \simeq \Gamma_X(E_F) \,. \end{displaymath} \end{itemize} \end{prop} The statement for the colimit is corollary 3.3.4.6 in [[Higher Topos Theory|HTT]]. The statement for the limit is corollary 3.3.3.4. \begin{remark} \label{}\hypertarget{}{} The form of the statement in prop. \ref{InfinityGroupoidalCoLimitsViaIntegrationAndSlicing} is the special case of the general form of [[internal (co-)limits]], here internal to the [[(∞,1)-topos]] [[∞Grpd]] with $Core(\inftyGrpd_{small})$ its small [[object classifier]]. See at \emph{\href{internal+%28co-%29limit#ExamplesInfinityGroupoidal}{internal (co-)limit -- Groupoidal homotopy (co-)limits}} for more on this. \end{remark} \hypertarget{ColimitsInInfinityCat}{}\subsubsection*{{Limits and colimits with values in $(\infty,1)$Cat}}\label{ColimitsInInfinityCat} \begin{prop} \label{}\hypertarget{}{} For $F : D \to$ [[(∞,1)Cat]] an [[(∞,1)-functor]], its $\infty$-colimit is given by forming the [[(∞,1)-Grothendieck construction]] $\int F$ of $F$ and then inverting the [[Cartesian morphism]]s. Formally this means, with respect to the [[model structure for Cartesian fibrations]] that there is a [[natural isomorphism]] \begin{displaymath} \lim_\to F \simeq (\int F)^\sharp \end{displaymath} in the [[homotopy category]] of the presentation of $(\infty,1)$-category by [[marked simplicial sets]]. \end{prop} This is [[Higher Topos Theory|HTT, corollary 3.3.4.3]]. For the special case that $F$ takes values in ordinary categories see also at [[2-limit]] the section \href{http://ncatlab.org/nlab/show/2-limit#2ColimitsInCat}{2-limits in Cat}. \hypertarget{limits_in_functor_categories}{}\subsubsection*{{Limits in $\infty$-functor categories}}\label{limits_in_functor_categories} For $C$ an ordinary [[category]] that admits small [[limit]]s and [[colimit]]s, and for $K$ a [[small category]], the [[functor category]] $Func(D,C)$ has all small limits and colimits, and these are computed objectwise. See [[limits and colimits by example]]. The analogous statement is true for an [[(∞,1)-category of (∞,1)-functors]]. \begin{prop} \label{}\hypertarget{}{} Let $K$ and $C$ be [[quasi-categories]], such that $C$ has all [[limit in a quasi-category|colimits]] indexed by $K$. Let $D$ be a small quasi-category. Then \begin{itemize}% \item The [[(∞,1)-category of (∞,1)-functors]] $Func(D,C)$ has all $K$-indexed colimits; \item A morphism $K^\triangleright \to Func(D,C)$ is a colimiting cocone precisely if for each object $d \in D$ the induced morphism $K^\triangleright \to C$ is a colimiting cocone. \end{itemize} \end{prop} \begin{proof} This is [[Higher Topos Theory|HTT, corollary 5.1.2.3]] \end{proof} \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[limit]], [[internal limit]] \item [[2-limit]] \item \textbf{$(\infty,1)$-limit} \begin{itemize}% \item [[finite (∞,1)-limit]], [[relative (∞,1)-limit]] \item [[homotopy limit]] \item [[lax (∞,1)-colimit]] \end{itemize} \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \hypertarget{general}{}\subsubsection*{{General}}\label{general} The definition of limit in quasi-categories is due to \begin{itemize}% \item [[André Joyal]], \emph{Quasi-categories and Kan complexes} Journal of Pure and Applied Algebra 175 (2002), 207-222. \end{itemize} A brief survey is on page 159 of \begin{itemize}% \item [[André Joyal]], \emph{The theory of quasicategories and its applications} lectures at \href{http://www.crm.es/HigherCategories/}{Simplicial Methods in Higher Categories}, (\href{http://www.crm.cat/HigherCategories/hc2.pdf}{pdf}) \end{itemize} A detailed account is in \href{http://arxiv.org/PS_cache/math/pdf/0608/0608040v4.pdf#page=48}{definition 1.2.13.4, p. 48} in \begin{itemize}% \item [[Jacob Lurie]], \emph{[[Higher Topos Theory]]} \end{itemize} \begin{itemize}% \item [[Denis-Charles Cisinski]], \emph{Do homotopy limits compute limits in the associated quasicategory in the non-combinatorial model category case?}, \href{http://mathoverflow.net/questions/176111/do-homotopy-limits-compute-limits-in-the-associated-quasicategory-in-the-non-com/176142#176142}{MO/176111/176142}. \end{itemize} A discussion of [[weighted limit|weighted]] $(\infty,1)$-limits is in \begin{itemize}% \item Martina Rovelli, \emph{Weighted limits in an (∞,1)-category}, 2019, \href{https://arxiv.org/abs/1902.00805}{arxiv:1902.00805} \end{itemize} \hypertarget{in_homotopy_type_theory}{}\subsubsection*{{In homotopy type theory}}\label{in_homotopy_type_theory} A formalization of some aspects of $(\infty,1)$-limits in terms of [[homotopy type theory]] is [[Coq]]-coded in \begin{itemize}% \item [[Guillaume Brunerie]], \emph{\href{https://github.com/guillaumebrunerie/HoTT/tree/master/Coq/Limits}{HoTT/Coq/Limits}} \end{itemize} See also \begin{itemize}% \item [[Egbert Rijke]], \emph{Homotopy Colimits and a Descent Theorem}, March 14, 2013 (\href{http://video.ias.edu/univalent-1213-0314-EgbertRijke}{video}) \end{itemize} [[!redirects limit in a quasi-category]] [[!redirects limits in a quasi-category]] [[!redirects colimit in a quasi-category]] [[!redirects colimits in a quasi-category]] [[!redirects limit in quasi-categories]] [[!redirects limits in quasi-categories]] [[!redirects colimit in quasi-categories]] [[!redirects colimits in quasi-categories]] [[!redirects limit in a quasicategory]] [[!redirects colimit in a quasicategory]] [[!redirects limit in quasicategories]] [[!redirects limits in quasicategories]] [[!redirects colimit in quasicategories]] [[!redirects colimits in quasicategories]] [[!redirects (infinity,1)-limit]] [[!redirects (infinity,1)-colimit]] [[!redirects (infinity,1)-limits]] [[!redirects (infinity,1)-colimits]] [[!redirects (∞,1)-limit]] [[!redirects (∞,1)-colimit]] [[!redirects (∞,1)-limits]] [[!redirects (∞,1)-colimits]] [[!redirects (∞,1)-product]] [[!redirects (∞,1)-coproduct]] [[!redirects (∞,1)-products]] [[!redirects (∞,1)-coproducts]] [[!redirects (∞,1)-pushout]] [[!redirects (∞,1)-pushouts]] [[!redirects limit in an (infinity,1)-category]] [[!redirects limits in an (infinity,1)-category]] [[!redirects limits in (infinity,1)-categories]] [[!redirects limit in an (∞,1)-category]] [[!redirects limits in an (∞,1)-category]] [[!redirects limits in (∞,1)-categories]] [[!redirects colimit in an (infinity,1)-category]] [[!redirects colimits in an (infinity,1)-category]] [[!redirects colimits in (infinity,1)-categories]] [[!redirects colimit in an (∞,1)-category]] [[!redirects colimits in an (∞,1)-category]] [[!redirects colimits in (∞,1)-categories]] [[!redirects (∞,1)-powering]] [[!redirects (∞,1)-tensoring]] [[!redirects (∞,1)-copower]] \end{document}