better fixity for ∘ptd, unit-l lemma
suspension fmap
two pushouts lemma cleanup
flip pushout cleanup
expand results on pathovers at pointed function types
long cofiber sequence