PULLBACK

PULLBACK

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

Definitions

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

is a together with the projection maps making the second diagram commute up to homotopy .

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

> (Homotopy Pullback Square). A homotopy pullback or cospan is called a homotopy pullback square if there exists a homotopy equivalence satisfying and . Map is called induced map.

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)

(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)