inverse functor defined (type checked version)
	modified:   Completeness.agda