| name | elements-infinity-cats |
| description | Elements of ∞-Category Theory (Riehl-Verity) for foundational ∞-categorical |
| version | 1.0.0 |
Elements of ∞-Categories Skill: Model-Independent Foundations
Status: ✅ Production Ready Trit: 0 (ERGODIC - coordinator) Color: #26D826 (Green) Principle: ∞-categories via model-independent axioms Frame: Riehl-Verity ∞-cosmos formalism
Overview
Elements of ∞-Category Theory provides model-independent foundations for ∞-categories. Rather than committing to quasi-categories, complete Segal spaces, or another model, the ∞-cosmos framework captures the common structure.
- ∞-cosmos: Enriched category of ∞-categories
- Isofibrations: Right class of factorization system
- Comma ∞-categories: Slice constructions
- Adjunctions/equivalences: Model-independent definitions
Core Framework
∞-cosmos K has:
- Objects: ∞-categories
- Mapping spaces: Kan complexes Map_K(A, B)
- Isofibrations: p : E ↠ B with lift property
- Comma objects: A/f for f : A → B
class InfinityCosmos k where
type Ob k :: Type
mapping :: Ob k → Ob k → KanComplex
isofibration :: (e : Ob k) → (b : Ob k) → Prop
comma :: {a b : Ob k} → (f : Map a b) → Ob k
Key Concepts
1. ∞-Cosmos Structure
-- Core axioms of an ∞-cosmos
record ∞-Cosmos : Type₁ where
field
Ob : Type
Hom : Ob → Ob → KanComplex
id : (A : Ob) → Hom A A
_∘_ : Hom B C → Hom A B → Hom A C
-- Limits
terminal : Ob
product : Ob → Ob → Ob
pullback : {A B C : Ob} → Hom A C → Hom B C → Ob
-- Isofibrations
isofib : {E B : Ob} → Hom E B → Prop
factorization : (f : Hom A B) →
Σ E, Σ (p : Hom E B), isofib p × trivial-cofib(A → E)
2. Comma ∞-Categories
-- Comma construction
comma : {K : ∞-Cosmos} {A B C : K.Ob}
→ K.Hom A C → K.Hom B C → K.Ob
comma f g = pullback (mapping-isofib A C f) (ev₀ : C^𝟚 → C)
×_{C} pullback (mapping-isofib B C g) (ev₁ : C^𝟚 → C)
-- Slice as comma
slice : {K : ∞-Cosmos} (B : K.Ob) (b : pt → B) → K.Ob
slice B b = comma (id B) b
3. Adjunctions
-- Model-independent adjunction
record Adjunction (L : Hom A B) (R : Hom B A) : Type where
field
unit : id A ⇒ R ∘ L
counit : L ∘ R ⇒ id B
triangle-L : (counit ∘ L) ∘ (L ∘ unit) ≡ id L
triangle-R : (R ∘ counit) ∘ (unit ∘ R) ≡ id R
Commands
# Verify ∞-cosmos axioms
just infinity-cosmos-check structure.rzk
# Compute comma construction
just comma-category f.rzk g.rzk
# Check adjunction conditions
just adjunction-verify L.rzk R.rzk
Integration with GF(3) Triads
yoneda-directed (-1) ⊗ elements-infinity-cats (0) ⊗ synthetic-adjunctions (+1) = 0 ✓ [Yoneda-Adjunction]
covariant-fibrations (-1) ⊗ elements-infinity-cats (0) ⊗ rezk-types (+1) = 0 ✓ [Model Transport]
Related Skills
- synthetic-adjunctions (+1): Generate adjunction data
- covariant-fibrations (-1): Validate fibration conditions
- segal-types (-1): Concrete Segal space model
Skill Name: elements-infinity-cats Type: ∞-Cosmos Coordinator Trit: 0 (ERGODIC) Color: #26D826 (Green)
Scientific Skill Interleaving
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
Graph Theory
- networkx [○] via bicomodule
- Universal graph hub
Bibliography References
category-theory: 139 citations in bib.duckdb
Cat# Integration
This 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
GF(3) Naturality
The skill participates in triads satisfying:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.