simplify sectioning and hypotheses in Functorish
cancelL_isequiv should not be an Instance (can't guess f)
track axioms more carefully in ReflectiveSubuniverse
implicit arguments to O_functor
more functoriality of O
use modalities for functoriality in Truncations
reflectors preserve products
WIP Freudenthal
Add an INCOMPLETE note to freudenthal
Merge pull request #485 from mikeshulman/functor

Functoriality and product-preservation of reflective subuniverses
Merge pull request #489 from JasonGross/wip-freudenthal-suspension-theorem

Make freudenthal suspension theorem compile
Fix frudenthal, reorder Truncation_functor args

Now, when you [apply Truncation_functor], you're not left with a goal of
[Univalence].  However, this isn't a satisfactory solution; perhaps
@mikeshulman can help solve the remaining goal involving
[truncation_incl] and [Truncation_functor] which used to go through
judgmentally?
Merge pull request #492 from JasonGross/fix-freudenthal

Fix frudenthal, reorder Truncation_functor args
Bind various scopes to their corresponding types

This gives better automatic scope resolution.