Fix the proof of isequiv_isepimorphism_ismonomorphism in Functor/Attributes,
using the new proof of isepi -> issurj using the mapping cone. There remains
to prove that Cf is an hSet in Pushout.v, which requires the general theory
of truncated colimits. One needs to use cumulativity to put Contr_unit in any
level i >= Set, and do some path lifting in Sum.v otherwise this will require
the whole proof to work on hSet@{Set} only.
Files forgotten in the last commit.
One less red needed in Contr_lift proof.
Minor fixes to make the whole of categories compile. Some explicit universes are
needed in Sum to avoid minimizing levels to Set (a better heuristic would be needed
to avoid that). I had to admit one proof in Adjoint/Composition/Core. Yoneda goes
through quickly thanks to a simpl and a few refines behave better than apply.