Galois Connections

galois-connections - Lawful Conversions via Adjoint Pairs

Overview

A Galois connection between preorders P and Q is a pair of monotone maps f :: P → Q and g :: Q → P such that:

f(x) ≤ y  ⟺  x ≤ g(y)

We say f is the left/lower adjoint and g is the right/upper adjoint.

Source: Fong & Spivak, Seven Sketches in Compositionality §1.4.1

┌─────────────────────────────────────────────────────────────────────────────┐
│                         GALOIS CONNECTION                                    │
├─────────────────────────────────────────────────────────────────────────────┤
│                                                                              │
│      P ─────────f────────→ Q       f = left adjoint (floor-like)            │
│      │                     │       g = right adjoint (ceiling-like)         │
│      │    f(x) ≤ y         │                                                │
│      │       ⟺             │       When f ⊣ g ⊣ h (adjoint string):         │
│      │    x ≤ g(y)         │         • f = floor                            │
│      │                     │         • g = round (nearest)                  │
│      Q ←────────g──────────P         • h = ceiling                          │
│                                                                              │
└─────────────────────────────────────────────────────────────────────────────┘

Source: cmk/connections

Based on cmk/connections - Haskell library for Galois connections.

Key insight: Adjoint strings of length 3 (f ⊣ g ⊣ h) enable lawful rounding:

-- Adjoint string: f ⊣ g ⊣ h
ordbin :: Cast k Ordering Bool
ordbin = Cast f g h
  where
    f LT = False    -- floor (lower adjoint)
    f _  = True

    g False = LT    -- round (middle)
    g True = GT

    h GT = True     -- ceiling (upper adjoint)
    h _  = False

Behaviors Lifted from Galois Connections

Behavior 1: floor (Left Adjoint)

def floor_behavior(connection, x):
    """
    Floor: greatest lower bound in target that is ≤ source.
    
    floor(x) = max { y : f(y) ≤ x }
    
    Properties:
    - Monotone: x₁ ≤ x₂ ⟹ floor(x₁) ≤ floor(x₂)
    - Deflationary: floor(x) ≤ x (when embedded)
    - Idempotent: floor(floor(x)) = floor(x)
    """
    return connection.left_adjoint(x)

Use case: Safely convert Float → Int without overflow.

Behavior 2: ceiling (Right Adjoint)

def ceiling_behavior(connection, x):
    """
    Ceiling: least upper bound in target that is ≥ source.
    
    ceiling(x) = min { y : x ≤ g(y) }
    
    Properties:
    - Monotone: x₁ ≤ x₂ ⟹ ceiling(x₁) ≤ ceiling(x₂)
    - Inflationary: x ≤ ceiling(x) (when embedded)
    - Idempotent: ceiling(ceiling(x)) = ceiling(x)
    """
    return connection.right_adjoint(x)

Use case: Round up to next representable value.

Behavior 3: round (Middle of Adjoint String)

def round_behavior(connection, x):
    """
    Round: nearest value in target (ties to even).
    
    Requires adjoint string f ⊣ g ⊣ h.
    round(x) = g(x) where g is the middle adjoint.
    
    Properties:
    - round(x) minimizes |x - round(x)|
    - Ties go to even (banker's rounding)
    """
    return connection.middle_adjoint(x)

Use case: Convert with minimal error.

Behavior 4: truncate (Toward Zero)

def truncate_behavior(connection, x):
    """
    Truncate: round toward zero.
    
    truncate(x) = floor(x) if x ≥ 0 else ceiling(x)
    
    Properties:
    - |truncate(x)| ≤ |x|
    - truncate(-x) = -truncate(x)
    """
    if x >= 0:
        return connection.left_adjoint(x)
    else:
        return connection.right_adjoint(x)

Use case: Integer division semantics.

Behavior 5: inner/outer (Interval Bounds)

def inner_outer_behavior(connection, x):
    """
    Inner/Outer: find the interval containing x in target type.
    
    inner(x) = the unique target value equal to x (if representable)
    outer(x) = (floor(x), ceiling(x)) bounding interval
    
    Properties:
    - If inner(x) exists: outer(x) = (inner(x), inner(x))
    - Otherwise: floor(x) < x < ceiling(x)
    """
    lo = connection.left_adjoint(x)
    hi = connection.right_adjoint(x)
    if lo == hi:
        return ("exact", lo)
    else:
        return ("interval", (lo, hi))

Use case: Precision analysis (is 1/7 exactly representable as Float?).

Behavior 6: lift (Function Lifting)

def lift_behavior(connection, f, x):
    """
    Lift: compute function in higher precision, round result.
    
    lift(f)(x) = round(f(embed(x)))
    
    Avoids precision loss in intermediate computation.
    """
    embedded = connection.embed(x)  # Go to higher precision
    result = f(embedded)            # Compute there
    return connection.round(result) # Come back

Use case: Avoid Float precision loss by computing in Double.

Implementation Patterns

Python Implementation

# /// script
# requires-python = ">=3.11"
# dependencies = []
# ///

from dataclasses import dataclass
from typing import TypeVar, Generic, Callable

P = TypeVar('P')  # Source type
Q = TypeVar('Q')  # Target type

@dataclass
class GaloisConnection(Generic[P, Q]):
    """A Galois connection between preorders P and Q."""
    
    left: Callable[[P], Q]   # f: P → Q (floor-like)
    right: Callable[[Q], P]  # g: Q → P (ceiling-like)
    
    def floor(self, x: P) -> Q:
        return self.left(x)
    
    def ceiling(self, x: P) -> Q:
        # ceiling via adjunction: min { y : x ≤ g(y) }
        return self.right(x)
    
    def is_adjoint(self, x: P, y: Q, le_P, le_Q) -> bool:
        """Verify adjunction: f(x) ≤ y ⟺ x ≤ g(y)"""
        return le_Q(self.left(x), y) == le_P(x, self.right(y))

@dataclass 
class AdjointString(Generic[P, Q]):
    """Adjoint string f ⊣ g ⊣ h for lawful rounding."""
    
    floor: Callable[[P], Q]    # f: left adjoint
    round: Callable[[P], Q]    # g: middle (both left and right)
    ceiling: Callable[[P], Q]  # h: right adjoint
    
    def truncate(self, x: P, zero: P, le) -> Q:
        if le(zero, x):
            return self.floor(x)
        else:
            return self.ceiling(x)

# Example: Float32 ↔ Int32
def make_f32_i32_connection() -> AdjointString[float, int]:
    import math
    return AdjointString(
        floor=lambda x: int(math.floor(x)) if math.isfinite(x) else None,
        round=lambda x: round(x) if math.isfinite(x) else None,
        ceiling=lambda x: int(math.ceil(x)) if math.isfinite(x) else None,
    )

Julia Implementation

"""
Galois connection between preorders.
"""
struct GaloisConnection{P,Q}
    left::Function   # f: P → Q
    right::Function  # g: Q → P
end

floor(gc::GaloisConnection, x) = gc.left(x)
ceiling(gc::GaloisConnection, x) = gc.right(x)

# Verify adjunction property
function is_adjoint(gc::GaloisConnection, x, y; leP=(≤), leQ=(≤))
    leQ(gc.left(x), y) == leP(x, gc.right(y))
end

"""
Adjoint string f ⊣ g ⊣ h for full rounding suite.
"""
struct AdjointString{P,Q}
    floor::Function    # f
    round::Function    # g
    ceiling::Function  # h
end

truncate(as::AdjointString, x, zero=0) = x ≥ zero ? as.floor(x) : as.ceiling(x)

# Example: Rational ↔ Float32
const rat_f32 = AdjointString{Rational,Float32}(
    r -> prevfloat(Float32(r)),  # floor
    r -> Float32(r),              # round
    r -> nextfloat(Float32(r)),  # ceiling
)

Domain Connections Table

Lawvere's Derivation: Logical Operations as Adjoints

The deepest application of Galois connections is Lawvere's derivation of propositional logic from adjoints. Given a C-set X (domain of discourse), the preorder Sub(X) of subobjects supports:

┌─────────────────────────────────────────────────────────────────────────────┐
│                    LOGICAL CONNECTIVES FROM ADJOINTS                         │
├─────────────────────────────────────────────────────────────────────────────┤
│                                                                              │
│  Operation      │ Symbol │  Adjoint Of        │  Formula                    │
│  ───────────────┼────────┼────────────────────┼─────────────────────────────│
│  Conjunction    │   ∧    │  Δ (right adjoint) │  C ≤ A∧B ⟺ C≤A and C≤B     │
│  Disjunction    │   ∨    │  Δ (left adjoint)  │  A∨B ≤ C ⟺ A≤C and B≤C     │
│  Implication    │   ⇒    │  (−)∧B (right)     │  A∧B ≤ C ⟺ A ≤ B⇒C         │
│  Subtraction    │   \    │  B∨(−) (left)      │  A ≤ B∨C ⟺ A\B ≤ C         │
│  Negation       │   ¬    │  derived: A⇒⊥      │  ¬A = largest disjoint      │
│  Complement     │   ∼    │  derived: ⊤\A      │  ∼A = smallest covering     │
│                                                                              │
└─────────────────────────────────────────────────────────────────────────────┘

Bi-Heyting Topos: Why C-Sets Have Two Negations

For a graph schema C = {E ⇉ V}, sub-C-sets (subgraphs) have both:

• ¬A ("not-A"): All elements not reachable from A
• ∼A ("non-A"): All elements reachable from non-A

The intrinsic boundary is: ∂A = A ∧ ∼A

# Subgraph logic operations via Galois connections
def negation(A, X):
    """¬A = largest subobject disjoint from A"""
    return {x for x in X if not any_edge_to(x, A)}

def complement(A, X):
    """∼A = smallest subobject covering X with A"""
    return {x for x in X if any_edge_from_outside(x, A)}

def boundary(A, X):
    """∂A = intrinsic boundary (vertices touching outside)"""
    return intersection(A, complement(A, X))

def induced_subgraph(A):
    """¬¬A = all edges between vertices in A"""
    return negation(negation(A))

def expand(A):
    """∼¬A = A expanded one degree outward"""
    return complement(negation(A))

def contract(A):
    """¬∼A = A contracted one degree inward"""
    return negation(complement(A))

Excluded Middle and Discreteness

The law of excluded middle (A ∨ ¬A = ⊤) holds for a C-set iff it is discrete (no morphisms). For graphs: no edges means classical logic.

Reference: Patterson & Myers, "Graphs and C-sets IV: The propositional logic of subgraphs" (2021)

Connection to Other Skills

DisCoPy (rigid categories)

• Cup/Cap = Unit/Counit of adjunction
• Left dual a.l ⊣ Right dual a.r

HoTT (univalence)

• Limit ⊣ Diagonal ⊣ Colimit
• Unit-counit formalization

CEREBRUM (case system)

• NOM-ACC ⊣ ERG-ABS alignment adjunction
• Case transitions as Galois connections

ACSets (C-set databases)

• Sub(X) forms bi-Heyting algebra
• Logical queries via adjoint operations

Plurigrid ASI

• GF(3) triplets are Galois-connected
• Attacker⊣Arbiter⊣Defender adjoint string
• Skill dispersal respects adjunction laws

Harmonization Engine

• harmonize.py galois shows known connections
• harmonize.py missing finds candidates

Exa Discovery Queries

# Find Galois connection libraries
mcp__exa__web_search_exa(
    query="Galois connection Haskell Julia Python implementation floor ceiling",
    numResults=10
)

# Find adjunction papers
mcp__exa__web_search_exa(
    query="site:arxiv.org adjoint functor Galois connection type theory",
    numResults=10
)

Justfile Recipes

# List known Galois connections
galois-list:
    @echo "🔗 Known Galois Connections"
    @echo "Float32 ↔ Int32: floor/ceiling/round"
    @echo "Float64 ↔ Float32: prevfloat/nextfloat"
    @echo "Rational ↔ Float32: exact bounds"
    @echo "Ordering ↔ Bool: ordbin connection"

# Floor conversion
galois-floor src dst val:
    @echo "floor({{val}}) :: {{src}} → {{dst}}"
    python3 -c "import math; print(int(math.floor({{val}})))"

# Ceiling conversion
galois-ceiling src dst val:
    @echo "ceiling({{val}}) :: {{src}} → {{dst}}"
    python3 -c "import math; print(int(math.ceil({{val}})))"

# Outer interval
galois-outer src dst val:
    @echo "outer({{val}}) :: {{src}} → ({{dst}}, {{dst}})"
    python3 -c "import math; x={{val}}; print(f'({int(math.floor(x))}, {int(math.ceil(x))})')"

Plurigrid ASI Adjoint String

The GF(3) bisimulation game forms an adjoint string:

Attacker (-1) ⊣ Arbiter (0) ⊣ Defender (+1)

           α (attack)                     δ (defend)
    MINUS ─────────────→ ERGODIC ─────────────→ PLUS
      │                     │                     │
      │   α(m) ≤ e         │                     │ e ≤ δ(p)
      │       ⟺            │       ⟺            │
      │   m ≤ verify(e)    │   attack(e) ≤ p    │
      │                     │                     │
    MINUS ←────────────── ERGODIC ←────────────── PLUS
           verify (γ)                  retreat (ρ)

GF(3) Conservation as Adjunction Law:

def gf3_adjoint_string(attacker, arbiter, defender):
    """
    Attacker ⊣ Arbiter ⊣ Defender forms adjoint string.

    Conservation: (-1) + (0) + (+1) = 0

    Properties:
    - attack ∘ verify = id (up to arbiter approval)
    - retreat ∘ defend = id (up to arbiter approval)
    """
    assert (attacker + arbiter + defender) % 3 == 0
    return AdjointString(
        floor=lambda e: max_attack(e),      # Attacker: maximize disruption
        round=lambda e: verify(e),           # Arbiter: verify balance
        ceiling=lambda e: min_defense(e),    # Defender: minimize exposure
    )

Skill Dispersal via Galois Adjunction

async def disperse_skill_galois(skill_path: str, agents: list):
    """
    Disperse skills using Galois connection structure.

    The adjunction ensures:
    - No information loss (unit η is injective)
    - No information gain (counit ε is surjective)
    - GF(3) conservation maintained
    """
    gc = gf3_adjoint_string(-1, 0, +1)

    for i, agent in enumerate(agents):
        trit = (i % 3) - 1  # Cycle: -1, 0, +1

        if trit == -1:
            # Attacker: floor (aggressive rounding)
            agent.receive(gc.floor(skill_path))
        elif trit == 0:
            # Arbiter: round (balanced)
            agent.receive(gc.round(skill_path))
        else:
            # Defender: ceiling (conservative rounding)
            agent.receive(gc.ceiling(skill_path))

    # Verify GF(3) conservation
    assert sum(a.trit for a in agents) % 3 == 0

See Also

• cmk/connections - Haskell source
• haskellari/lattices - Lattice primitives
• AlgebraicJulia/Catlab.jl - Full adjunction machinery
• gh-skill-explorer - Discovery skill that found this
• discopy - Rigid categories with adjoint duals
• moebius-inversion - Incidence algebras on posets
• acsets - C-set databases with bi-Heyting logic
• plurigrid-asi-integrated - GF(3) skill dispersal
• catsharp-galois - Scale Galois connections via Mazzola
• ~/Desktop/CanonicalC-SetContext.md - Full C-set reference with bi-Heyting logic

End-of-Skill Interface

Commands

# Show available connections
just galois-list

# Convert with floor
just galois-floor float32 int32 3.7

# Convert with ceiling  
just galois-ceiling float32 int32 3.7

# Show interval bounds
just galois-outer rational float32 "1/7"

# Lift function to higher precision
just galois-lift float32 float64 "lambda x: x**2 - 2*x + 1" 1.5

Autopoietic Marginalia

The interaction IS the skill improving itself.

Every use of this skill is an opportunity for worlding:

• MEMORY (-1): Record what was learned
• REMEMBERING (0): Connect patterns to other skills
• WORLDING (+1): Evolve the skill based on use

Add Interaction Exemplars here as the skill is used.

CT lattice atlas

Part of: para-mensch-commons (CT lattice family).