categories-functors
starsforks
How to install categories-functors?
parcadei/continuous-claude-v3/categories-functors
$npx -y skills add parcadei/Continuous-Claude-v3 --skill categories-functorsProblem-solving strategies for categories functors in category theory
SKILL.md
| 1 | # Categories Functors |
| 2 | |
| 3 | ## When to Use |
| 4 | |
| 5 | Use this skill when working on categories-functors problems in category theory. |
| 6 | |
| 7 | ## Decision Tree |
| 8 | |
| 9 | |
| 10 | 1. **Verify Category Axioms** |
| 11 | - Objects and morphisms (arrows) defined? |
| 12 | - Identity morphism for each object: id_A: A -> A |
| 13 | - Composition associative: (f . g) . h = f . (g . h) |
| 14 | - Write Lean 4: `theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc` |
| 15 | |
| 16 | 2. **Check Functor Properties** |
| 17 | - F: C -> D maps objects to objects, arrows to arrows |
| 18 | - Preserves identity: F(id_A) = id_{F(A)} |
| 19 | - Preserves composition: F(g . f) = F(g) . F(f) |
| 20 | - Write Lean 4: `theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp` |
| 21 | |
| 22 | 3. **Functor Types** |
| 23 | - Covariant: preserves arrow direction |
| 24 | - Contravariant: reverses arrow direction |
| 25 | - Faithful/Full: injective/surjective on Hom-sets |
| 26 | - Equivalence: full, faithful, essentially surjective |
| 27 | |
| 28 | 4. **Common Functors** |
| 29 | - Forgetful functor: forgets structure (e.g., Grp -> Set) |
| 30 | - Free functor: left adjoint to forgetful |
| 31 | - Hom functor: Hom(A, -) or Hom(-, B) |
| 32 | - Power set functor: Set -> Set via X |-> P(X) |
| 33 | |
| 34 | 5. **Verify with Lean 4** |
| 35 | - Compiler-in-the-loop: write proof, `lake build` checks |
| 36 | - Mathlib has full category theory library |
| 37 | - See: `.claude/skills/lean4-functors/SKILL.md` for exact syntax |
| 38 | |
| 39 | |
| 40 | ## Tool Commands |
| 41 | |
| 42 | ### Lean4_Category |
| 43 | ```bash |
| 44 | # Lean 4 with Mathlib: import CategoryTheory.Category.Basic |
| 45 | ``` |
| 46 | |
| 47 | ### Lean4_Functor |
| 48 | ```bash |
| 49 | # Lean 4: theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp |
| 50 | ``` |
| 51 | |
| 52 | ### Lean4_Build |
| 53 | ```bash |
| 54 | lake build # Compiler-in-the-loop verification |
| 55 | ``` |
| 56 | |
| 57 | ## Cognitive Tools Reference |
| 58 | |
| 59 | See `.claude/skills/math-mode/SKILL.md` for full tool documentation. |
People who liked this also viewed
6 picksType
- find-skillsHelps users discover and install agent skills when they ask questions like "how do I do X", "find a skill for X", "is there a skill that can...", or express interest in extending capabilities. This skSkillsJul 2026
- grill-meA relentless interview to sharpen a plan or design.SkillsJul 2026
- vercel-react-best-practicesVercel's official collection of agent skillsSkillsJul 2026
- improve-codebase-architectureScan a codebase for deepening opportunities, present them as a visual HTML report, then grill through whichever one you pick.SkillsJul 2026
- setup-matt-pocock-skillsConfigure this repo for the engineering skills — set up its issue tracker, triage label vocabulary, and domain doc layout. Run once before first use of the other engineering skills.SkillsJul 2026
- triageMove issues and external PRs through a state machine of triage roles — categorise, verify, grill if needed, and write agent-ready briefs.SkillsJul 2026
