install
source · Clone the upstream repo
git clone https://github.com/plurigrid/asi
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/infinity-topos" ~/.claude/skills/plurigrid-asi-infinity-topos && rm -rf "$T"
manifest:
skills/infinity-topos/SKILL.mdsource content
Infinity Topos Skill
∞-Topos theory unifying hatchery repos, worlds, and GA abelian extensions.
Trit: +1 (PLUS) — Generator/extension of topos-theoretic structures
Hatchery Repos
| Repo | Color | Index | Focus |
|---|---|---|---|
| #115A06 | 277 | Core ∞-topos theory |
| #90269E | 783 | Lean 4 ∞-categories |
| #72351B | 62 | Topos theory foundations |
| #5CE273 | 1003 | Applied topos |
| — | — | Pretopos structures |
| #969D34 | — | Topos-based OS |
∞-Topos Fundamentals
∞-Topos = (∞,1)-category satisfying: 1. Colimits: All small colimits exist 2. Descent: Effective epimorphisms 3. Universes: Object classifiers 4. Giraud axioms: ∞-categorical version
Giraud's ∞-Axioms
-- From plurigrid/infinity-cosmos structure InfinityTopos where C : ∞Category colim_complete : HasAllSmallColimits C descent : EffectiveEpis C universe : ObjectClassifier C -- Every ∞-topos is an ∞-category of ∞-sheaves theorem topos_is_sheaves (T : InfinityTopos) : T ≃ Sh∞(Site, Space) := by apply lurie_characterization
GA ↔ ∞-Topos Bridge
Abelian Extensions in ∞-Topoi
In an ∞-topos: Ext^n(A, B) ≃ π₀(Maps(A, B[n])) For Clifford grades: Ext¹(Cl^{k+1}, Cl^k) ≃ π₀(Ω^{-1} Maps(Cl^{k+1}, Cl^k)) ≃ grade filtration extensions
Central Extensions as Fiber Sequences
1 → ℤ/2 → Spin(n) → SO(n) → 1 In ∞-topos: BZ/2 → BSpin(n) → BSO(n) Fiber sequence classifies central extension via: H²(BSO(n); ℤ/2) = [BSO(n), B²ℤ/2]
World Mappings
| World | ∞-Topos Role | Hatchery Repo |
|---|---|---|
| A | ACSet as ∞-presheaf | |
| B | Terminal ∞-type | |
| C | Functional ∞-topos | — |
| D | Data ∞-sheaves | — |
| E | ∞-cosmos foundation | |
ACSet Schema for ∞-Topos
@present SchInfinityTopos(FreeSchema) begin # Objects at each level (Obj0, Obj1, Obj2, ObjN)::Ob # n-morphisms # Structure maps source::Hom(Obj1, Obj0) target::Hom(Obj1, Obj0) # Higher source/target s2::Hom(Obj2, Obj1) t2::Hom(Obj2, Obj1) # Composition (via colimit) compose::Hom(Obj1 ⊗ Obj1, Obj1) # Universal properties is_colimit::Attr(ObjN, Bool) is_classifier::Attr(Obj0, Bool) # GF(3) grading trit::Attr(Obj1, GF3Trit) end
Lurie's Characterization
∞-Topos ≃ Left exact localization of Psh∞(C) Where: Psh∞(C) = Fun(C^op, Space) -- ∞-presheaves Space = ∞-groupoids Localization at W ⊆ Psh∞(C): Sh∞(C,W) = Psh∞(C)[W⁻¹]
Higher Topos Theory Applications
Cohomology in ∞-Topoi
H^n(X; A) = π₀ Maps(X, K(A,n)) For GA: H^n(Cl-Mod; ℤ/3) classifies GF(3) extensions n=1: Ext¹ (abelian) n=2: Central extensions (spin structures)
Descent and Gluing
Descent datum in ∞-topos: Given cover U → X, section s : U → E Descent = isomorphism p₁*s ≃ p₂*s on U ×_X U For GA: Grade-respecting descent Cl^k bundle on X with GA transition functions
Integration with GA Skills
| GA Skill | ∞-Topos Connection |
|---|---|
| ga-abelian-extensions | Ext as Maps in stable ∞-cat |
| ga-central-extensions | Fiber sequences, H² |
| ga-derived-category | Stable ∞-category |
| clifford-acset-bridge | ∞-presheaf schema |
Triad
sheaf-cohomology (-1) ⊗ infinity-topos (+1) ⊗ effective-topos (0) = 0 ✓
Commands
# Explore hatchery repos cat /Users/bob/ies/hatchery_repos/bmorphism__infinity-topos/GAY.md cat /Users/bob/ies/hatchery_repos/plurigrid__infinity-cosmos/GAY.md # Lean 4 infinity-cosmos cd /Users/bob/ies/hatchery_repos/plurigrid__infinity-cosmos lake build # Check topos structure julia -e 'using Catlab; is_topos(C)'
References
- Lurie: Higher Topos Theory (HTT)
- Rezk: Toposes and homotopy toposes
- Riehl-Verity: Elements of ∞-Category Theory
skill (FloxHub)effective-topos
skillelements-infinity-cats
skillrezk-types
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.