From asi
Defines Segal types for synthetic ∞-categories ensuring unique binary composites up to homotopy. Supplies Rzk definitions, Lean4 structures, chemputer semantics, and Ruby composition example.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
> *"A Segal type is a type where binary composites exist uniquely up to homotopy."*
Defines Rezk types as complete Segal spaces with local univalence (isomorphisms ≃ identities) in Rzk. Includes Lean4 integration, chemical semantics, and Ruby examples for ∞-category work.
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.
"A Segal type is a type where binary composites exist uniquely up to homotopy." — Emily Riehl & Michael Shulman
Segal types are the synthetic ∞-categorical analogue of categories. They automatically ensure composition is coherently associative and unital at all dimensions.
#lang rzk-1
-- The directed interval (axiomatized)
#define 2 : CUBE
-- Hom type (directed paths)
#define hom (A : U) (x y : A) : U
:= (t : 2) → A [t ≡ 0₂ ↦ x, t ≡ 1₂ ↦ y]
-- 2-simplex (composite witness)
#define Δ² : CUBE
:= (t₁ : 2) × (t₂ : 2) × (t₁ ≤ t₂)
-- Composition witness type
#define hom2 (A : U) (x y z : A)
(f : hom A x y) (g : hom A y z) (h : hom A x z) : U
:= (σ : Δ²) → A [
σ = (0₂, t) ↦ f t,
σ = (t, 1₂) ↦ g t,
σ = (t, t) ↦ h t
]
-- Segal condition: unique composites
#define is-segal (A : U) : U
:= (x y z : A) → (f : hom A x y) → (g : hom A y z)
→ is-contr (Σ (h : hom A x z), hom2 A x y z f g h)
-- Segal type
#define Segal : U
:= Σ (A : U), is-segal A
| ∞-Category Concept | Chemical Interpretation |
|---|---|
| Objects | Chemical species |
| 1-morphisms (hom) | Reactions A → B |
| 2-morphisms (hom2) | Witnesses that pathways yield same product |
| Segal condition | Unique composite reactions |
| Coherent associativity | Reaction order doesn't matter (up to iso) |
segal-types (-1) ⊗ directed-interval (0) ⊗ rezk-types (+1) = 0 ✓
As a Validator (-1), segal-types verifies that:
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory
-- Segal space as simplicial space with Segal condition
structure SegalSpace where
X : SimplicalSpace
segal : ∀ n, IsEquiv (segalMap X n)
-- Composition in a Segal space
def compose {S : SegalSpace} {x y z : S.X 0}
(f : S.X 1 ⦃x, y⦄) (g : S.X 1 ⦃y, z⦄) : S.X 1 ⦃x, z⦄ :=
(S.segal 2).inv ⟨f, g⟩
# lib/segal_interaction.rb
module SegalInteraction
# Each interaction is a morphism in a Segal type
# Composition = sequential skill invocation
def self.compose_interactions(f, g)
# f : Interaction (skill A → skill B)
# g : Interaction (skill B → skill C)
# Result: unique composite f;g : (skill A → skill C)
composite_seed = (f.seed ^ g.seed) & MASK64
InteractionEntropy::Interaction.new(
{ composed: [f.id, g.id] }.to_json,
seed: composite_seed
)
end
end
Composition is coherent: All ways of associating a sequence of morphisms yield the same result (up to higher homotopy).
Identity exists: For each object x, there is id_x : hom A x x.
2-out-of-3: If two of f, g, g∘f are equivalences, so is the third.
| Speaker | Relevance | Repository/Talk |
|---|---|---|
| bmorphism | Category theory signatures | libc_zignatures |
| condret | ESIL semantics (∞-cat structure) | radare2 ESIL |
| thestr4ng3r | CFG as ∞-groupoid | r2ghidra |