restriction functors in completeness (without typechecking)
	modified:   Categories/Idems.agda
	modified:   Completeness.agda
	modified:   MonicClasses.agda