Natural equivalence of categories
Natural equivalence of categories

Coq now knows that [ComposeFunctor] repects natural equivalence of functors.

I've rewritten/re-proved all the lemmas about [FunctorsEquivalent] using
[FunctorsNaturallyEquivalent] instead.

I've defined [CategoriesNaturallyEquivalent], and proven that it's an
equivalence relation on categories.

I've been renaming the symmetry methods from [*_symm] to [*_sym] to match with
[eq_sym].

I suspect that there is a better way to do some of the proofs I've written,
especially things like [functors_equivalent_implies_natural_equivalence] and
the proof that [ComposeFunctors] respects [FunctorsNaturallyEquivalent].

CategoricalData/catdb,JasonGross/catdb,CategoricalData/catdb,JasonGross/catdb