inverse functor defined (problems during type checking)
	modified:   Completeness.agda