Add category of isomorphisms

[marcosh]

@sjoerdvisscher very nice!

I really liked the usage of cong2 instead of cong {f=...}