proving that the completeness functor preserves composition
	modified:   Completeness.agda