Synthetic Adjunctions

Synthetic Adjunctions Skill: Universal Construction Generation

Status: ✅ Production Ready Trit: +1 (PLUS - generator) Color: #D82626 (Red) Principle: Adjunctions generate universal structures Frame: Directed type theory with adjoint functors

Overview

Synthetic Adjunctions generates adjunction data in directed type theory. Adjunctions are the fundamental generators of universal constructions—limits, colimits, Kan extensions, and monads all arise from adjunctions.

1. Unit/counit: Natural transformations η, ε
2. Triangle identities: Coherence conditions
3. Mate correspondence: Bijection between hom-sets
4. Universal properties: Initial/terminal characterizations

Core Formula

L ⊣ R adjunction:
  η : Id → R ∘ L       (unit)
  ε : L ∘ R → Id       (counit)
  
Triangle identities:
  (εL) ∘ (Lη) = id_L
  (Rε) ∘ (ηR) = id_R

-- Generate adjunction from universal property
generate_adjunction :: FreeConstruction → Adjunction
generate_adjunction (Free F) = Adjunction {
    left = F,
    right = Forgetful,
    unit = η_universal,
    counit = ε_evaluation
}

Key Concepts

1. Adjunction Generation

-- Construct adjunction from representability
representable-adjunction : 
  (F : A → B) → (G : B → A) →
  ((a : A) (b : B) → Hom_B(F a, b) ≃ Hom_A(a, G b)) →
  Adjunction F G
representable-adjunction F G iso = record
  { unit = λ a → iso.inv (id (F a))
  ; counit = λ b → iso.to (id (G b))
  ; triangle-L = from-iso-naturality
  ; triangle-R = from-iso-naturality
  }

2. Free-Forgetful Generation

-- Generate free algebra adjunction
free-forgetful : (T : Monad) → Adjunction (Free T) (Forgetful T)
free-forgetful T = record
  { unit = T.η
  ; counit = T.μ ∘ T.map(eval)
  ; triangle-L = T.left-unit
  ; triangle-R = T.right-unit
  }

-- Free monoid on sets
Free-Mon : Adjunction Free Underlying
Free-Mon = free-forgetful List-Monad

3. Kan Extension via Adjunction

-- Left Kan extension as left adjoint to restriction
Lan : (K : A → B) → Adjunction (Lan_K) (Res_K)
Lan K = record
  { left = λ F → colim_{K/b} F ∘ proj
  ; right = λ G → G ∘ K
  ; unit = universal-arrow
  ; counit = eval-at-colimit
  }

4. Generate Limits from Adjunctions

-- Diagonal adjunction gives limits
limit-adjunction : Adjunction Δ lim
limit-adjunction = record
  { left = Δ         -- diagonal functor
  ; right = lim      -- limit functor
  ; unit = proj      -- projections
  ; counit = univ    -- universal property
  }

Commands

# Generate adjunction from free construction
just adjunction-generate --free-on Monoid

# Synthesize unit/counit
just adjunction-unit-counit L R

# Verify triangle identities
just adjunction-verify adj.rzk

Integration with GF(3) Triads

covariant-fibrations (-1) ⊗ directed-interval (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Transport]
yoneda-directed (-1) ⊗ elements-infinity-cats (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Yoneda-Adjunction]
segal-types (-1) ⊗ directed-interval (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Segal Adjunctions]

Related Skills

• elements-infinity-cats (0): Coordinate ∞-categorical adjunctions
• covariant-fibrations (-1): Validate fibration conditions
• free-monad-gen (+1): Generate free monads from adjunctions

Skill Name: synthetic-adjunctions Type: Universal Construction Generator Trit: +1 (PLUS) Color: #D82626 (Red)

Scientific Skill Interleaving

This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:

Graph Theory

• networkx [○] via bicomodule
  • Universal graph hub

Bibliography References

• category-theory: 139 citations in bib.duckdb

Cat# Integration

This skill maps to Cat# = Comod(P) as a bicomodule in the equipment structure:

Trit: 0 (ERGODIC)
Home: Prof
Poly Op: ⊗
Kan Role: Adj
Color: #26D826

GF(3) Naturality

The skill participates in triads satisfying:

(-1) + (0) + (+1) ≡ 0 (mod 3)

This ensures compositional coherence in the Cat# equipment structure.