HoTT/HoTT — pull request #631 by mikeshulman (2014-12-03 10:58:52+00:00)
Title: 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?)