the whole pullbackiso proof was marked irrelevant. Now only the required bits are.
	modified:   Categories/Pullbacks.agda