Moving quotients in completeness (first restriction functor completed)
	modified:   Completeness.agda