Module 7: The Adjoint Triple and Data Migration

The adjoint triple Σ ⊣ Δ ⊣ Π — left pushforward, base change, right pushforward — is the categorical engine of functorial data migration. Given any morphism of schemas, this triple provides three canonical ways to move data between them, each with a precise semantic interpretation: reindexing, lossy aggregation, and lossless extension. This module develops the triple in full and applies it to the synchronization of heterogeneous datasets. The lab session uses Catlab.jl to implement a real migration and demonstrate contradiction detection via delta lenses.

Learning Objectives

  • Define a schema morphism as a functor between schema categories and explain what it encodes.
  • Derive the adjoint triple Σ_f ⊣ Δ_f ⊣ Π_f from a schema morphism f: S → T.
  • Describe the semantic role of each functor: Δ reindexes, Σ aggregates (lossy), Π extends (lossless).
  • Implement a functorial data migration between two schemas in Catlab.jl.
  • Define a delta lens and explain how it enables bidirectional synchronization with put/get coherence.
  • Demonstrate how a symmetric lens surfaces contradictions between two heterogeneous models.

Materials

Key Concepts

Central Concepts from Prerequisites