Make the inverse of functor_forall transparent
Don't use isequiv_adjointify in equiv_sigT_corect

We don't need it.  But I needed to slightly change the destruction of a
sigma type in the recursion principle.
Merge pull request #315 from JasonGross/better-equiv_sigT_corect

Don't use isequiv_adjointify in equiv_sigT_corect
Merge pull request #313 from JasonGross/isequiv-functor-forall-transparent

Make the inverse of functor_forall transparent