uniformize reflective subuniverses and modalities
truncation is a modality
Clean up Pushout.v a bit
join
open and closed modalities
better naming for equivalence move functions
explicit Existing Instance *and* Coercion after typeclasses, for clarity
coqdoc comment
remove unnecessary imports
clarify comment about generalizing binders
comment about Local Instance
use Local Instance in PropositionalFracture
use Local Instance in Truncations
comment about _equiv naming
Typeclasses Transparent inO
comment: Local Instance works anywhere
missing Global in isequiv_O_rect
update PropositionalFracture to use transitivity
remove unnecessary import
Merge pull request #470 from mikeshulman/rsumod

Uniformize reflective subuniverses and modalities