AbstractThis is high-level formal approach to Data Integration. The goal was to model DI and model a high-level integration function and prove certain features (e.g. idempotency).