{- CW-Comlexes
   Copyright (c) Groupoid Infinity, 2014-2020.

   HoTT 6.6 Cell Complexes -}

module cw where
import suspension
import nat
import pushout

-- Cell complexes as attachment cells
attaching (A B C: U): U = B -> C -> A
attached (A B C: U) (a: attaching A B C): U
  = pushout A B (prod B C) (\(x: prod B C) -> a x.1 x.2)
                           (\(x: prod B C) -> x.1)