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