The modal factorization system

This is a formalization of most of section 7.5 and 7.6 in the book, in the generality of an arbitrary modality.  Pleasingly, all the theorems in `hit.Connectedness` that generalize to a modality (mainly, those that don't involve the interaction of multiple values of `n`) could be proven in that generality with essentially cut-and-pasted proofs, while the remaining theorems in `hit.Connectedness` still work where they are with essentially the same proofs (at least once I got the coercions and hints configured correctly).  The proof of lemma 7.6.5 is a bit trickier than in the book, because our `O_ind` has only a propositional computation rule.  I only found [one mistake](https://github.com/HoTT/book/pull/731) in the book.
*sigh*  I did check out the branch to come up with the `unfold ...; change ...` version.  But then I re-checked out set-keyed-unification and tried to build with a new version of trunk, and set up coq-bug-finder, so I had to check out this branch in a separate clone of the repo...

And the `repeat match goal` I pasted above works fine for me as a drop-in replacement for both `ev_equiv_compose` uses, on the pinned version of coq.  I still don't know why `change` complained with `Error: Failed to get enough information from the left-hand side to type the right-hand side.`, though.... @mattam82, any ideas?