added idem\cong
modified:   Categories/Idems.agda
modified:   Utilities.agda