defined completeness isomorphism.
	modified:   Completeness.agda
	modified:   Functors.agda