Extended [pullback_fmap] to pointed version.
Added by-hand version of the hfiber_to_Omega equivalence.
Long Exact Sequence theorem: two more admits down, two to go.