Lex modalities and the fracture theorem

Long-promised.  (-:  Some notes:

1. Also includes some general theory about pullbacks, in `Pullback.v`, and a notation `f^* g` for the pullback of `g` along `f`.
2. At first I tried making lex-ness a module type to be assumed on top of a modality module-type, as for accessibility.  But then I realized that since lex-ness is a "universe-local property" (unlike accessibility!) we can just make it a typeclass and allow ordinary universe polymorphism to kick in.
3. Given this, I was strongly tempted _not_ to include separate files `Lex` and `Topological`, putting the relevant theory into `Modality` or `Accessible` depending on whether it needs accessibility.  (This would even be possible for `Fracture`.)  This would have the advantage of avoiding the proliferation of `_Theory` modules and (presumably) solving the multiple-inheritance problem described in the comments in `Lex.v`.  I have so far resisted the temptation, but we'll see how annoyed I get in the future with the current setup.  (Would using `Include` instead of `Export`, if we trusted it to be anomaly-free, also solve these problems?)

Do you want `Check` statements to make sure that you're not accidentally identifying universes in the bodies of these definitions?