\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*{homotopy pullback}

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

\hypertarget{limits_and_colimits}{}\paragraph*{{$(\infty,1)$-Limits and colimits}}\label{limits_and_colimits}

[[!include infinity-limits - contents]]

\hypertarget{equality_and_equivalence}{}\paragraph*{{Equality and Equivalence}}\label{equality_and_equivalence}

[[!include equality and equivalence - contents]]

\hypertarget{homotopy_theory}{}\paragraph*{{Homotopy theory}}\label{homotopy_theory}

[[!include homotopy - contents]]

\hypertarget{model_category_theory}{}\paragraph*{{Model category theory}}\label{model_category_theory}

[[!include model category theory - 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{in_category_theory}{In category theory}\dotfill \pageref*{in_category_theory} \linebreak
\noindent\hyperlink{InHomotopyTypeTheory}{In homotopy type theory}\dotfill \pageref*{InHomotopyTypeTheory} \linebreak
\noindent\hyperlink{ConcreteConstructions}{Concrete constructions}\dotfill \pageref*{ConcreteConstructions} \linebreak
\noindent\hyperlink{ConstructionsGeneral}{General}\dotfill \pageref*{ConstructionsGeneral} \linebreak
\noindent\hyperlink{ConstructionInHomotopyTypeTheory}{In homotopy type theory}\dotfill \pageref*{ConstructionInHomotopyTypeTheory} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{HomotopyFiberCharacterization}{Fiber-wise characterization}\dotfill \pageref*{HomotopyFiberCharacterization} \linebreak
\noindent\hyperlink{pasting_law}{Pasting law}\dotfill \pageref*{pasting_law} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{fiber_sequences}{Fiber sequences}\dotfill \pageref*{fiber_sequences} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general_2}{General}\dotfill \pageref*{general_2} \linebreak
\noindent\hyperlink{ReferencesForHoTT}{In terms of homotopy type theory}\dotfill \pageref*{ReferencesForHoTT} \linebreak


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

A \textbf{homotopy pullback} is a special kind of [[homotopy limit]]: the appropriate notion of [[pullback]] in the context of [[homotopy theory]]. Homotopy pullbacks model the [[limit in quasi-categories|quasi-category pullbacks]] in the [[(infinity,1)-category]] that is [[presentable (infinity,1)-category|presented]] by a given [[homotopical category]]. Since pullbacks are also called fiber products, homotopy pullbacks are also called \textbf{homotopy fiber products}.

A \textbf{homotopy pushout} is the [[duality|dual]] concept.

For more details see [[homotopy limit]].

In the context of [[homotopy type theory]] a homotopy pullback is the [[categorical semantics|interpretation]] of the space of solutions to an [[equation]].

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

\hypertarget{in_category_theory}{}\subsubsection*{{In category theory}}\label{in_category_theory}

As with all homotopy limits, there is both a \emph{local} and a \emph{global} notion of homotopy pullback.

The \emph{global} definition says that the homotopy pullback of a [[co-span|cospan]] $X \to Z \leftarrow Y$ in a [[category with weak equivalences]] $C$ is its image under the right [[derived functor]] of the [[base change]] functor $pb: C^{\to \leftarrow} \to C$.

The \emph{local} definition says that the homotopy pullback of $X \to Z \leftarrow Y$ in a category with a notion of [[homotopy]] consists of a square

\begin{displaymath}
\itexarray{
   P & \to& Y
   \\
    \downarrow && \downarrow
   \\
   X &\to& Z
  }
\end{displaymath}
that [[commutative square|commutes]] up to [[homotopy]], and such that for any other square

\begin{displaymath}
\itexarray{
   T & \to& Y
   \\
    \downarrow && \downarrow
   \\
   X &\to& Z
  }
\end{displaymath}
that commutes up to homotopy, there exists a morphism $T\to P$, unique up to homotopy, making the two triangles commute up to homotopy, and similarly for homotopies and higher homotopies. In other words, there is an equivalence

\begin{displaymath}
Map(T,P) \simeq HoSq(T,X\to Z\leftarrow Y)
\end{displaymath}
between the space of maps $T\to P$ and the space of homotopy commutative squares with vertex $T$.

In good situations, such as when $X,Y,Z$ are [[fibrant object|fibrant]] in a [[model category]], the two constructions agree up to weak equivalence.

Note that in both cases, there is a canonical map from the actual pullback $X\times_Z Y$ to the homotopy pullback $X\times_Z^h Y$. In the global case this comes by the definition of a derived functor; in the local case it comes because a commutative square is, in particular, a homotopy commutative one.

\hypertarget{InHomotopyTypeTheory}{}\subsubsection*{{In homotopy type theory}}\label{InHomotopyTypeTheory}

In [[homotopy type theory]] the homotopy pullback of a [[term]] of [[function type]]

\begin{displaymath}
f : A \to C
\end{displaymath}
along a term of function type

\begin{displaymath}
g : B \to C
\end{displaymath}
is given formally by precisely the same formula that would also define the ordinary [[fiber product]] of functions of sets, namely by

\begin{displaymath}
\left\{
     a : A, b : B \;\; | \;\; f(a) = g(b)
  \right\}
  \,.
\end{displaymath}
Spelled out, this is the [[dependent sum]]

\begin{displaymath}
\underset{
    \itexarray{
      {a \colon A}  
      \\
      {b\colon B}
    }
   }{\sum} (f(a)= g(b))
\end{displaymath}
over the [[dependent type|dependent]] [[identity type]] over the [[evaluation]] of $f$ and $g$.

What in classical logic is interpreted as the set of pairs $(a,b)$ such that $f(a)$ and $g(b)$ are equal here becomes the restriction of a [[mapping cocylinder]].

Formal proof that this is the homotopy pullback in homotopy type theory is in (\hyperlink{Brunerie}{Brunerie}). Proof in the [[categorical semantics of homotopy type theory]] is \hyperlink{ConstructionInHomotopyTypeTheory}{below}.

\hypertarget{ConcreteConstructions}{}\subsection*{{Concrete constructions}}\label{ConcreteConstructions}

We discuss various concrete constructions by ordinary [[pullbacks]] and ordinary [[limits]] such that under some sufficient conditions these compute homotopy pullbacks, up to weak equivalence.

\hypertarget{ConstructionsGeneral}{}\subsubsection*{{General}}\label{ConstructionsGeneral}

\begin{prop}
\label{HomotopyPullbackByOrdinaryPullback}\hypertarget{HomotopyPullbackByOrdinaryPullback}{}
Let $A \to C \leftarrow B$ be a [[diagram]] in some [[model category]]. Then sufficient conditions for the ordinary (1-categorical) [[pullback]] $A \times_C B$ to present the homotopy pullback of the diagram are

\begin{itemize}%
\item one of the two morphisms is a [[fibration]] and all three objects are [[fibrant objects]];


\item one of the two morphisms is a [[fibration]] and the model category is [[right proper model category|right proper]].



\end{itemize}
\end{prop}
Both statements are classical. They are reviewed for instance as \hyperlink{Lurie}{Lurie, prop. A.2.4.4}. The proof of the second statement is spelled out \href{proper+model+category#HomotopyLimits}{here}.

\begin{remark}
\label{}\hypertarget{}{}
Notice that a fibrant [[resolution]] of the diagram in the injective [[model structure on functors]] has \emph{both} morphisms be a fibration. So the first point in prop. \ref{HomotopyPullbackByOrdinaryPullback} says that (in the special case of pullbacks) something weaker than this is sufficient for computing the [[homotopy limit]] of the diagram.

This can be explained in model-categorical terms by the fact that the category of [[cospans]] also has a [[Reedy model structure]] in which the fibrant objects are precisely those considered in the first point above, and that homotopy limits can equally well be computed using this model structure (specifically, the [[adjunction]] $Const \dashv Lim$ is [[Quillen adjunction|Quillen]] with respect to it).

In this spirit one may ask for the largest class of morphisms such that their ordinary pullbacks are already homotopy pullbacks. This is related to the concept of \emph{[[sharp morphisms]]}.

\end{remark}
Due to prop. \ref{HomotopyPullbackByOrdinaryPullback} one typically computes homotopy pullbacks of a diagram by first forming a [[resolution]] of one of the two morphisms by a fibration and then forming an ordinary pullback.

\begin{cor}
\label{HomotopyPullbackByFactorizationLemma}\hypertarget{HomotopyPullbackByFactorizationLemma}{}
If in $A \stackrel{f}{\to} C \stackrel{g}{\leftarrow} B$ all three objects are [[fibrant objects]], then the homotopy pullback of this diagram is presented by the ordinary [[pullback]]

\begin{displaymath}
\itexarray{
     A\times_C^h B & \to & C^I \times_C B
    \\
    \downarrow && \downarrow 
    \\
     A & \stackrel{f}{\to} & C
  }
  \,.
\end{displaymath}
or, equivalently up to [[isomorphism]], as the ordinary [[pullback]]

\begin{displaymath}
\itexarray{
     A\times_C^h B & \to & C^I
    \\
    \downarrow && \downarrow 
    \\
     A\times B & \stackrel{(f,g)}{\to} & C\times C
  }
  \,.
\end{displaymath}
\end{cor}
See also at \emph{[[Mayer-Vietoris sequence]]} \href{Mayer-Vietoris+sequence#SequenceFromDiagonal}{this proposition}.

\begin{proof}
Since the objects are already fibrant, prop. \ref{HomotopyPullbackByOrdinaryPullback} implies that it is sufficient to replace one of the morphisms by a fibrant resolution. Such a resolution is provided by the [[factorization lemma]]: by \href{factorization+lemma#FibrantResolution}{Lemma 3}, $B \to C$ admits a canonical fibrant resolution

\begin{displaymath}
C^I \times_C B \twoheadrightarrow C
\end{displaymath}
where $C \stackrel{\simeq}{\to} C^I \to C \times C$ is a [[path space object]] for $C$ (for instance, when $C$ is a [[closed monoidal homotopical category]] then this can be taken to be the [[internal hom]] with an [[interval object]] $I$).

\end{proof}
The homotopy pullback constructed in this way is an example of a \emph{strict homotopy limit}, as mentioned at [[homotopy limit]]. In such a case, one can say that an arbitrary homotopy-commutative square

\begin{displaymath}
\itexarray{
   W & \to& Y
   \\
    \downarrow && \downarrow
   \\
   X &\to& Z
  }
\end{displaymath}
is a homotopy pullback square if the induced morphism from $W$ to the strict homotopy pullback is a [[weak equivalence]].

A useful class of examples of this is implied by the following:

\begin{prop}
\label{}\hypertarget{}{}
Let $\mathcal{C}$ be a category of [[simplicial presheaves]] over some [[site]] equipped with a \emph{local} injective [[model structure on simplicial presheaves]] with respect to that site.

Then an ordinary pullback of $A \to C \leftarrow B$ in $\mathcal{C}$ is a homotopy pullback already when one of the two morphisms is an objectwise [[Kan fibration]].

\end{prop}
\begin{proof}
The \emph{global} projective [[model structure on simplicial presheaves]] is [[right proper model category|right proper]]. So by prop. \ref{HomotopyPullbackByOrdinaryPullback} the ordinary pullback in question presents the homotopy pullback in the global structure. By the discussion at [[homotopy limit]] and [[Bousfield localization of model categories]], this presents the [[(∞,1)-pullback]] of the diagram of [[(∞,1)-presheaves]], and the fibrant replacement of that pullback in the \emph{local} model structure presents the [[(∞,1)-sheafification]] of this [[(∞,1)-presheaf]]. This is (essentially by definition, see [[(∞,1)-topos]]) a [[left exact functor|left exact]] [[(∞,1)-functor]] and hence preserves finite [[(∞,1)-limits]].

\end{proof}
\hypertarget{ConstructionInHomotopyTypeTheory}{}\subsubsection*{{In homotopy type theory}}\label{ConstructionInHomotopyTypeTheory}

If we unwind the [[categorical semantics]] of the \hyperlink{InHomotopyTypeTheory}{above definition}

\begin{displaymath}
A \times_C^h B \simeq \{ a : A, b : B | (f(a) = g(b)) \}
\end{displaymath}
of the homotopy pullback in [[homotopy type theory]], we re-obtain the \hyperlink{ConstructionsGeneral}{above prescription} for how to construct homotopy pullbacks.

So let the ambient category be a suitable [[type-theoretic model category]].

\begin{example}
\label{}\hypertarget{}{}
The type $a : A, b : B \vdash (f(a) = g(b))$ is obtained by [[substitution]] from the [[identity type]] of $C$. By the discussion there, the [[categorical semantics]] of substitution is given by [[pullback]] of the fibrations that interpret the [[dependent types]], and so this is interpreted as the pullback $[a : A, b : B \vdash (f(a) = g(b))] \coloneqq (f,g)^* C^I$ of the [[path space object]] of $C$:

\begin{displaymath}
\itexarray{
    [a : A, b : B \vdash (f(a) = g(b))]
    &\to&
    [Id C]
    \\
    \downarrow && \downarrow
    \\
    [a : A , b : B]
    &\stackrel{(f,g)}{\to}&
    [c_1 : C , c_2 : C]
  }
  \;\;
   = 
  \;\;
  \itexarray{
    (f,g)^* C^I &\to& C^I
    \\
    \downarrow && \downarrow
    \\
    A \times B
    &
    \stackrel{(f,g)}{\to}
    &
    C \times C
  }
  \,.
\end{displaymath}
Forming the [[dependent sum]] over $a : A, b : B$ is simply interpreted as regarding the resulting object $(f,g)^* C^I$ as an object in $\mathcal{C} \simeq \mathcal{C}_{/*}$ instead of as an object in the [[slice category]] $\mathcal{C}_{/ A \times B}$.

Since by assumption on the categorical interpretation of a type, all objects here are fibrant, this coincides with the expression of the homotopy pullback from corollary \ref{HomotopyPullbackByFactorizationLemma} above.

\end{example}
\begin{example}
\label{}\hypertarget{}{}
Specifically, let $f \colon A \longrightarrow B$ be a [[function]], then the [[categorical semantics]] for the expression

\begin{displaymath}
\underset{b \colon B}{\sum} fib(f,b)
  =
  \underset{b \colon B}{\sum} \underset{a \colon A}{\sum} (f(a) = b)
\end{displaymath}
is the canonical [[fibration]] replacement of $f$ as it appears notably in the [[factorization lemma]]

\begin{displaymath}
\itexarray{
    A \times_B B^I &\longrightarrow& B^I
    \\
    \downarrow && \downarrow
    \\
    A \times B
    &\stackrel{(f, Id)}{\longrightarrow}&
    B \times B
  }
  \,.
\end{displaymath}
\end{example}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{HomotopyFiberCharacterization}{}\subsubsection*{{Fiber-wise characterization}}\label{HomotopyFiberCharacterization}

\begin{prop}
\label{FiberwiseCharacterizationInInfinityGrpds}\hypertarget{FiberwiseCharacterizationInInfinityGrpds}{}
In plain [[homotopy types]] (i.e. in [[∞-groupoids]], in the standard [[model structure on simplicial sets]] etc.) the following holds:

a [[diagram]]

\begin{displaymath}
\itexarray{
    A &\stackrel{f}{\longrightarrow}& B
    \\
    \downarrow && \downarrow^{\mathrlap{p}}
    \\
    C &\stackrel{g}{\longrightarrow}& D
  }
\end{displaymath}
is a homotopy pullback diagram precisely if it induces a [[weak equivalence]] on all [[homotopy fibers]]

\begin{displaymath}
\itexarray{
    hfib_b(f) &\longrightarrow& A &\stackrel{f}{\longrightarrow}& B
    \\
    \downarrow^{\mathrlap{\simeq}}  && \downarrow && \downarrow^{\mathrlap{p}}
    \\
    hfib_{p(b)}(g) &\longrightarrow& C &\stackrel{g}{\longrightarrow}& D
  }
\end{displaymath}
for all elements $b \in B$.

\end{prop}
(e.g. \hyperlink{CPS05}{CPS 05, 5.2}, \href{http://mathoverflow.net/a/192303/381}{MO})

\begin{remark}
\label{}\hypertarget{}{}
For the analog of prop. \ref{FiberwiseCharacterizationInInfinityGrpds} to hold in [[(∞,1)-categories]] more general than [[∞-groupoids]] one would need either ``enough [[global elements]]'' of the object $B$ to detect all homotopy fibers, or else one would need a suitable ``[[internal logic|internal]]'' formulation of the statement.

\end{remark}
On the other hand in [[stable homotopy theory]] the statement holds generally:

\begin{prop}
\label{FiberwiseRecognitionInStableCase}\hypertarget{FiberwiseRecognitionInStableCase}{}
For $\mathcal{C}$ a [[stable model category]], then for a diagram

\begin{displaymath}
\itexarray{
    A &\stackrel{f}{\longrightarrow}& B
    \\
    \downarrow && \downarrow^{\mathrlap{p}}
    \\
    C &\stackrel{g}{\longrightarrow}& D
  }
\end{displaymath}
the following are equivalent

\begin{enumerate}%
\item the square is a homotopy pullback square;


\item the square is a [[homotopy pushout]] squre;


\item the induced morphism on the homotopy fiber over the [[zero object]] 0 is a weak equivalence

\begin{displaymath}
hfib_0(f) \stackrel{\simeq}{\longrightarrow} hfib_0(g)
   \,.
\end{displaymath}


\end{enumerate}
\end{prop}
A proof in terms of [[stable model categories]] including the third item is spelled out for instance in (\hyperlink{Hovey07}{Hovey 07, remark 7.1.12}). (Beware: this is not in the original volume from 1999, but is in the version ``reprinted with corrections'' from 2007.) A proof in terms of [[stable (∞,1)-categories]] of the first two items is in ([[Higher Algebra|Lurie HA, prop. 1.1.3.4 (2)]]).

\hypertarget{pasting_law}{}\subsubsection*{{Pasting law}}\label{pasting_law}

\begin{itemize}%
\item [[pasting law]]

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

\hypertarget{fiber_sequences}{}\subsubsection*{{Fiber sequences}}\label{fiber_sequences}

Of particular interest are consecutive homotopy pullbacks of point inclusions. These give rise to [[fiber sequence]]s and [[loop space object]]s.

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

\begin{itemize}%
\item [[equation]]


\item [[homotopy limit]]


\item [[(∞,1)-pullback]], [[(∞,1)-limit]]



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

\hypertarget{general_2}{}\subsubsection*{{General}}\label{general_2}

See the references at \emph{[[homotopy limit]]} .

Fairly comprehensive resources are

\begin{itemize}%
\item [[Mark Hovey]], \emph{Model categories}, Mathematical Surveys and Monographs, vol 63, 1999,reprinted 2007


\item [[Jacob Lurie]], appendix of \emph{[[Higher Topos Theory]]}



\end{itemize}
See also

\begin{itemize}%
\item [[Wojciech Chacholski]], Wolfgang Pitsch, and [[Jerome Scherer]], \emph{Homotopy pullback squares up to localization}, in [[Dominique Arlettaz]], [[Kathryn Hess]] (eds.) \emph{An Alpine Anthology of Homotopy Theory} (\href{http://arxiv.org/abs/math/0501250}{arXiv:math/0501250}, \href{http://sma.epfl.ch/~jscherer/articles/hopullbacks2.pdf}{pdf}, \href{http://dx.doi.org/10.1090/conm/399}{doi:10.1090/conm/399})

\end{itemize}
\hypertarget{ReferencesForHoTT}{}\subsubsection*{{In terms of homotopy type theory}}\label{ReferencesForHoTT}

A proposal for a formalization of homotopy pushouts by [[higher inductive types]] in [[homotopy type theory]] has been given in

\begin{itemize}%
\item [[Mike Shulman]], \emph{Homotopy Type Theory VI} (\href{http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html}{blog post})

\end{itemize}
A [[homotopy type theory|HoTT]]-[[Coq]]-coding of homotopy pullbacks and pushouts is in

\begin{itemize}%
\item [[Guillaume Brunerie]], \emph{\href{https://github.com/guillaumebrunerie/HoTT/blob/master/Coq/Limits/Pullbacks.v}{HoTT/Coq/Limits/Pullbacks.v}}

\end{itemize}
[[!redirects homotopy pullback]] [[!redirects homotopy pullbacks]]

[[!redirects homotopy pushout]] [[!redirects homotopy pushouts]]

[[!redirects homotopy fiber product]] [[!redirects homotopy fiber products]]



\end{document}