Synthetic adjunctions in directed type theory for ∞-categorical universal constructions.
Status: ✅ Production Ready Trit: +1 (PLUS - generator) Color: #D82626 (Red) Principle: Adjunctions generate universal structures Frame: Directed type theory with adjoint functors
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.
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
}
-- 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
}
-- 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
-- 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
}
-- 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
}
# 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
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]
Skill Name: synthetic-adjunctions Type: Universal Construction Generator Trit: +1 (PLUS) Color: #D82626 (Red)