maybe the functor definition is done, have to type check it on Andri's computer.
	modified:   Completeness.agda