Introduce saturated identity natural transformation
Introduce saturated identity natural transformation

Also start using setoid for equivalence relations.  This made the identity
natural transformation proof much easier, but also significantly complicated
the proof of [saturate].  I'll have to work on re-automating the [saturate]
proof in a nice way.

I'm not sure why I need a separate parametric relation for each equivalence
relation, rather than being able to do it once for [RelationsEquivalent].

As it says in a comment in the source, I had to do
  Add Parametric Relation C s d : _ (PathsEquivalence C s d)
and not
  Add Parametric Relation C s d : _ (PathsEquivalent C s d)
though I'm not sure why.  If I don't, I get the error
  Error: Unable to manage a dependent metavariable of higher-order type.

I also got
  Toplevel input, characters 0-27:
  Anomaly: unknown meta ?2167. Please report.
at some point, though I don't remember where, and didn't feel like making a
minimal test case for it.  I think it was when I told Coq to apply something
like RelationsEquivalent without passing any parameters?

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