Asi infinity-topos

Infinity Topos Skill

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.md
source 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

RepoColorIndexFocus
bmorphism/infinity-topos
#115A06277Core ∞-topos theory
plurigrid/infinity-cosmos
#90269E783Lean 4 ∞-categories
TeglonLabs/topoi
#72351B62Topos theory foundations
plurigrid/topos
#5CE2731003Applied topos
bmorphism/pretopos
Pretopos structures
TeglonLabs/topOS
#969D34Topos-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 RoleHatchery Repo
AACSet as ∞-presheaf
plurigrid/topos
BTerminal ∞-type
bmorphism/infinity-topos
CFunctional ∞-topos
DData ∞-sheaves
E∞-cosmos foundation
plurigrid/infinity-cosmos

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-extensionsExt as Maps in stable ∞-cat
ga-central-extensionsFiber sequences, H²
ga-derived-categoryStable ∞-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
  • effective-topos
    skill (FloxHub)
  • elements-infinity-cats
    skill
  • rezk-types
    skill

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.