{- Homotopy Pushout:
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 6.8 Pushouts -}

module pushout where
import proto
import pullback
import nat

-- Homotopy Colimit
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) ]


-- data |-| (A : U) = f (x: A) | e (a b : A), f a = f b

-- Colimit of Propositional Truncations A_{n+1} = pTrunc_{A_n}
data colimit (A : nat -> U)
             (f : (n : nat) -> A n -> A (succ n))
   = ix (n : nat) (x: A n)
   | gx (n : nat) (a: A n) <i> [ (i=0) -> ix (succ n) (f n a)
                               , (i=1) -> ix n a]

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

--      f
--  A ----> B
--  |   po  | po2
--  V       V
--  1 ----> cofiber_f
--     po1

-- TODO: cofiberPushout