categories-functors skill
Problem-solving strategies for categories functors in category theory
A100/100content scan
Is the categories-functors skill safe?
Clean: nothing in its files matched our rules. We read 1 file in the folder on 2026-09-28.
No findings.
Install the categories-functors skill
A skill is a folder. Copy it into your agent's skills folder and the agent loads it when the task matches its description.
git clone --depth 1 https://github.com/parcadei/Continuous-Claude-v3.git /tmp/Continuous-Claude-v3 mkdir -p ~/.claude/skills cp -r /tmp/Continuous-Claude-v3/.claude/skills/math/category-theory/categories-functors ~/.claude/skills/categories-functors
available in every project
In the Claude apps, zip the folder and upload it from the Skills settings. The folder on GitHub
The instructions your agent would load
SKILL.md as published, without the frontmatter. Read it on GitHub
Categories Functors
When to Use
Use this skill when working on categories-functors problems in category theory.
Decision Tree
- Verify Category Axioms
- Objects and morphisms (arrows) defined?
- Identity morphism for each object: id_A: A -> A
- Composition associative: (f . g) . h = f . (g . h)
- Write Lean 4: theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc
- Check Functor Properties
- F: C -> D maps objects to objects, arrows to arrows
- Preserves identity: F(idA) = id{F(A)}
- Preserves composition: F(g . f) = F(g) . F(f)
- Write Lean 4: theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp
- Functor Types
- Covariant: preserves arrow direction
- Contravariant: reverses arrow direction
- Faithful/Full: injective/surjective on Hom-sets
- Equivalence: full, faithful, essentially surjective
- Common Functors
- Forgetful functor: forgets structure (e.g., Grp -> Set)
- Free functor: left adjoint to forgetful
- Hom functor: Hom(A, -) or Hom(-, B)
- Power set functor: Set -> Set via X |-> P(X)
- Verify with Lean 4
- Compiler-in-the-loop: write proof, lake build checks
- Mathlib has full category theory library
- See: .claude/skills/lean4-functors/SKILL.md for exact syntax
Tool Commands
Lean4_Category
# Lean 4 with Mathlib: import CategoryTheory.Category.BasicLean4_Functor
# Lean 4: theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_compLean4_Build
lake build # Compiler-in-the-loop verificationCognitive Tools Reference
See .claude/skills/math-mode/SKILL.md for full tool documentation.
More skills from parcadei/Continuous-Claude-v3
- Aagent-context-isolationAgent Context Isolation
- Aagent-orchestrationAgent Orchestration Rules
- Aagentic-workflowAgentic Workflow Pattern
- Aagentica-claude-proxyGuide for integrating Agentica SDK with Claude Code CLI proxy
- Aagentica-infrastructureReference guide for Agentica multi-agent infrastructure APIs
- Aagentica-promptsWrite reliable prompts for Agentica/REPL agents that avoid LLM instruction ambiguity
- Aagentica-sdkBuild Python agents with Agentica SDK - @agentic decorator, spawn(), persistence, MCP integration
- Aagentica-serverAgentica server + Claude proxy setup - architecture, startup sequence, debugging
- Aagentica-spawnSpawn Agentica multi-agent patterns
- Aanalytic-functionsProblem-solving strategies for analytic functions in complex analysis
- Aast-grep-findAST-based code search and refactoring via ast-grep MCP
- Aasync-repl-protocolAsync REPL Protocol