Define based identity systems

[anshwad10]

I was working on proving the equivalence between functional relations and functions in #1252, and I found myself wanting to prove (f a ≡ b) ≡ R a b while having precisely the data for showing that R a is a based identity system at f a (in the sense of the 1lab). I know this means I could prove it directly, however I think it would be more useful to define (based) identity systems somewhere (perhaps Foundations.IdentitySystem or Relation.Binary.IdentitySystem) and prove that every based identity system is equal to Path.

[anshwad10]

So I temporarily put identity systems in Relation.Binary.Properties but I think they should be in Foundations, because I plan to use them in #1237