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.
Ok, now the `match` version works for me too.  I wonder why it didn't before.  Also, adding `| [ |- context[equiv_fun (equiv_inverse ?f) ?a] ] => change ((equiv_inverse f) a) with (f^-1 a)` to the second case eliminates the need for the duplication of `O_hfiber_O_fact_inverse_beta`.

What would you think about wrapping this match up in a tactic, like `ev_equiv` or something, maybe even defined in `Basics/Equivalences`?