added RestFun\cong
modified:   Categories/Idems.agda
modified:   RestrictionFunctors.agda
modified:   Utilities.agda