added epis, idempotents and split epis and proved that there is a unique iso between two splittings for the same epi.
modified:   Categories.agda