PUSHOUT

(Span). The two maps with the same domain are called span:

(Homotopy Pushout). The homotopy pushout or homotopy colimit (denoted as ) of the span diagram:

where is an equivalence relation and for . If is a based space with basepoint , we add the relation for all .

data pushout (A B C: U) (f: C -> A) (g: C -> B)
   = po1 (_: A)
   | po2 (_: B)
   | po3 (c: C) <i> [ (i = 0) -> po1 (f c) ,
                      (i = 1) -> po2 (g c) ]

EXAMPLES

(Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U
  = pullback A unit B f (\(x: unit) -> y)

(Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B)
  : pullbackSq (hofiber A B f y)

(Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U
  = pushout A unit B f (\(x: B) -> tt)

(Kernel).

kernel (A B: U) (f: A -> B): U
  = pullback A A B f f

(Cokernel).

cokernel (A B: U) (f: B -> A): U
  = pushout A A B f f

LITERATURE

[1]. Brian Munson and Ismar Volić. Cubical Homotopy Theory