natural-transformations
starsforks
How to install natural-transformations?
parcadei/continuous-claude-v3/natural-transformations
$npx -y skills add parcadei/Continuous-Claude-v3 --skill natural-transformationsProblem-solving strategies for natural transformations in category theory
SKILL.md
| 1 | # Natural Transformations |
| 2 | |
| 3 | ## When to Use |
| 4 | |
| 5 | Use this skill when working on natural-transformations problems in category theory. |
| 6 | |
| 7 | ## Decision Tree |
| 8 | |
| 9 | |
| 10 | 1. **Verify Naturality** |
| 11 | - eta: F => G is natural transformation between functors F, G: C -> D |
| 12 | - For each f: A -> B in C, diagram commutes: |
| 13 | G(f) . eta_A = eta_B . F(f) |
| 14 | - Write Lean 4: `theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality` |
| 15 | |
| 16 | 2. **Component Analysis** |
| 17 | - eta_A: F(A) -> G(A) for each object A |
| 18 | - Each component is morphism in target category D |
| 19 | - Lean 4: `def η : F ⟶ G where app := fun X => ...` |
| 20 | |
| 21 | 3. **Natural Isomorphism** |
| 22 | - Each component eta_A is isomorphism |
| 23 | - Functors F and G are naturally isomorphic |
| 24 | - Notation: F ≅ G (NatIso in Mathlib) |
| 25 | |
| 26 | 4. **Functor Category** |
| 27 | - [C, D] has functors as objects |
| 28 | - Natural transformations as morphisms |
| 29 | - Vertical composition: Lean 4 `CategoryTheory.NatTrans.vcomp` |
| 30 | - Horizontal composition: `CategoryTheory.NatTrans.hcomp` |
| 31 | |
| 32 | 5. **Yoneda Lemma Application** |
| 33 | - Nat(Hom(A, -), F) ~ F(A) naturally in A |
| 34 | - Lean 4: `CategoryTheory.yonedaEquiv` |
| 35 | - Fully embeds C into [C^op, Set] |
| 36 | - See: `.claude/skills/lean4-nat-trans/SKILL.md` for exact syntax |
| 37 | |
| 38 | |
| 39 | ## Tool Commands |
| 40 | |
| 41 | ### Lean4_Naturality |
| 42 | ```bash |
| 43 | # Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality |
| 44 | ``` |
| 45 | |
| 46 | ### Lean4_Nat_Trans |
| 47 | ```bash |
| 48 | # Lean 4: def η : F ⟶ G where app := fun X => component_X |
| 49 | ``` |
| 50 | |
| 51 | ### Lean4_Yoneda |
| 52 | ```bash |
| 53 | # Lean 4: CategoryTheory.yonedaEquiv -- Yoneda lemma |
| 54 | ``` |
| 55 | |
| 56 | ### Lean4_Build |
| 57 | ```bash |
| 58 | lake build # Compiler-in-the-loop verification |
| 59 | ``` |
| 60 | |
| 61 | ## Cognitive Tools Reference |
| 62 | |
| 63 | 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
