PULLBACK

$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

Pullback package contains basic information about Homotopy Limits known as Pullbacks.

Definitions

Definition (Homotopy Pullback). The pullback of the first diagram (which is called cospan)

$$ \begin{array}{ccc} & & B \\ & & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array} $$

$$ \begin{array}{ccc} A \times^{h}_{C} B & \mapright{\mathbf{pb_2}} & B \\ \mapdown{\mathbf{pb_1}} & \mapdiagl{\mathbf{pb_3}} & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array} $$

$$ A \times^{h}_{C} B = \Sigma_A\Sigma_B C^I \\ = \left\{ (x,y,h) : \Sigma_X\Sigma_Y C^I | h(0)=f(x), h(1)=g(y) \right\} $$

is a $X \times^h_C Y$ together with the projection maps $pb_{1,2,3}$ making the second diagram commute up to homotopy $H(x,y,h,t) = h(t)$.

pullback (A B C:U) (f: A -> C) (g: B -> C): U = (a: A) * (b: B) * Path C (f a) (g b)

pb1 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> A = \(x: pullback A B C f g) -> x.1
pb2 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> B = \(x: pullback A B C f g) -> x.2.1
pb3 (A B C: U) (f: A -> C) (g: B -> C): (x: pullback A B C f g) -> Path C (f x.1) (g x.2.1)
  = \(x: pullback A B C f g) -> x.2.2

Definition (Homotopy Pullback Square). A homotopy pullback or cospan is called a homotopy pullback square if there exists a homotopy equivalence $\phi : Z \rightarrow A \times_C^h B$ satisfying $z_1 : Z \rightarrow A = pb_1 \circ \phi$ and $z_2: Z \rightarrow B = pb_2 \circ \phi$. Map $\phi$ is called induced map.

$$ \begin{array}{ccc} X \times^{h}_{C} Y & \mapright{\mathbf{pb_2}} & B \\ \mapdown{\mathbf{pb_1}} & \square_{(Z,z_1,z_2)} & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array} $$

induced (Z A B C: U) (f: A -> C) (g: B -> C)
        (z1: Z -> A) (z2: Z -> B)
        (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
      : Z -> pullback A B C f g
      = \(z: Z) -> ((z1 z),(z2 z),h z)

pullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B): U
         = (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
         * isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

isPullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B)
             (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)): U
           = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

Proposition (Existence of Pullback Square). Pullback Square exists and equals Pullback, where induced map is identity. Given as 2.11 Exercise in HoTT Chapter 2.

completePullback (A B C: U) (f: A -> C) (g: B -> C) :
    pullbackSq (pullback A B C f g) A B C f g (pb1 A B C f g) (pb2 A B C f g)