Both functors are ok now (with a postulate for the second).
	modified:   Completeness.agda