git clone https://github.com/plurigrid/asi
T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/topos-polynomial-functors" ~/.claude/skills/plurigrid-asi-topos-polynomial-functors && rm -rf "$T"
skills/topos-polynomial-functors/SKILL.mdTopos Polynomial Functors Skill
Polynomial functors and dialectica categories following Topos Institute's formalization by David Spivak, Nelson Niu, and Valeria de Paiva.
Core Concepts
The Poly Category
Poly is the category of polynomial functors with remarkable structure:
- Complete and cocomplete
- 3 orthogonal factorization systems
- 2 monoidal closed structures (⊗ composition, × parallel)
Free Sum and Product Completion: ΣΠC
Objects of ΣΠC are formal expressions:
∑_{i∈I} ∏_{a∈A_i} c_{i,a}
Key distributive law (products of sums ↔ sums of products):
∏_{i∈I} ∑_{a∈A_i} c_{i,a} ≅ ∑_{ā∈∏_{i∈I}A_i} ∏_{i∈I} c_{i,ā_i}
Polynomial Structure: Positions, Directions, Predicates
For polynomial
p = ∑_{i∈I} y^{A_i}:
- Positions (I): Where we are
- Directions (A_i): Where we can go from position i
- Predicates: Properties at each position/direction pair
Morphisms in ΣΠC
A morphism
φ: p → q consists of:
- Forward on positions:
φ₁: I_p → I_q - Backward on directions:
φ♯: A_{q,φ₁(i)} → A_{p,i} - Forward on predicates:
φ₂: c_{p,i,a} → c_{q,φ₁(i),φ♯(a)}
Vertical-Cartesian Factorization
Every morphism factors as vertical then cartesian:
- Vertical: Only changes position (identity on directions)
- Cartesian: Only changes directions/predicates (identity on positions)
p --vertical--> r --cartesian--> q
Monomials: Mo(C)
Monomials are polynomials with single position:
Mo(C) ⊂ ΣΠC where objects are ∏_{a∈A} c_a
Monomials correspond to bimorphic lenses in functional programming.
Dialectica Categories
D(Set) - Dialectica Sets
Objects: (U, X, α: U×X → 2) Morphisms: (f, F) where f: U → V, F: U×Y → X with α(u,F(u,y)) ⊢ β(f(u),y)
G(Set) - Gödel Dialectica
Like D(Set) but with total relations.
Gd(C) - Generalized Dialectica
Parameterized by base category C with fibration structure.
Bridge: Dialectica = ΣΠ(2) with predicate structure
Key Formulas
Polynomial Functor Application
p(Y) = ∑_{i∈I} Y^{A_i} = ∑_{i∈I} (A_i → Y)
Lens as Polynomial Morphism
Lens(S,T,A,B) ≅ Hom_Poly(Sy^S, Ty^A×B)
Monoidal Composition
(p ⊗ q)(Y) = p(q(Y)) p ⊗ q = ∑_{i∈I_p} ∑_{j∈I_q^{A_i}} y^{∑_{a∈A_i} B_{j(a)}}
Usage Patterns
Define a Polynomial
# p(y) = 2y³ + y = ∑_{i∈{0,1}} y^{A_i} # where A_0 = 3, A_1 = 1 poly_p = Polynomial( positions = [:left, :right], directions = Dict(:left => 3, :right => 1) )
Compose Polynomials
# (p ⊗ q)(y) = p(q(y)) composed = poly_compose(p, q)
Vertical-Cartesian Factor
v, c = factor_vc(morphism) # morphism = c ∘ v
Cross-Skill Synergies
| Skill | Connection |
|---|---|
| Games as polynomial coalgebras |
| D(Set) ≅ ΣΠ(2) with predicates |
| Position=color, direction=trit |
| Poly has all Kan extensions |
| Polynomial schemas for C-sets |
Quick Reference
ΣΠC = Free sum-product completion Poly = ΣΠ(Set) Mo(C) = Monomials ⊂ ΣΠC D(Set) = Dialectica = ΣΠ(2) + predicates Morphism = (forward-pos, backward-dir, forward-pred) Factor = Vertical ; Cartesian
End-of-Skill Interface
Integration with Gay-MCP
Map polynomial structure to color generation:
# Positions → Colors (deterministic from seed) # Directions → Trits (GF(3) backward map) # Predicates → Validation (forward on properties) struct PolyColor position::UInt64 # seed/index → color directions::NTuple{3, Int8} # trit triple predicate::Bool # validation result end
Integration with Open Games
Polynomial functors model open games:
Game(X,S,R,Y) ≅ Lens(X×S, Y×R) ≅ ∑_{σ:X→Y} ∏_{x:X} R → S
- Positions = Strategy profiles
- Directions = Deviations
- Predicates = Equilibrium conditions
Integration with Dialectica Skill
Dialectica ──────────────────────── Poly │ │ │ D(Set) ≅ ΣΠ(2) │ │ with predicate fibration │ │ │ ▼ ▼ Proof-relevant Compositional game semantics open systems
References
- Spivak, Niu: "Polynomial Functors: A Mathematical Theory of Interaction"
- de Paiva: "Dialectica Categories"
- Topos Institute Blog: poly.math.mit.edu
- Ahman, Uustalu: "Directed Containers as Categories"
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.