From asi
Generates synthetic adjunctions in directed type theory, including unit/counit, triangle identities, and universal constructions like free-forgetful, Kan extensions, and limits.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
**Status**: ✅ Production Ready
Provides model-independent foundations for ∞-categories using Riehl-Verity ∞-cosmos framework. Verifies axioms, computes comma categories, and checks adjunctions with Agda/Haskell examples.
Guides Next.js Cache Components and Partial Prerendering (PPR): 'use cache' directives, cacheLife(), cacheTag(), revalidateTag() for caching, invalidation, static/dynamic optimization. Auto-activates on cacheComponents: true.
Guides building MCP servers enabling LLMs to interact with external services via tools. Covers best practices, TypeScript/Node (MCP SDK), Python (FastMCP).
Share bugs, ideas, or general feedback.
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)
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
category-theory: 139 citations in bib.duckdbThis 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
The skill participates in triads satisfying:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.