split up the functor into separate parts
	modified:   Completeness.agda