Agent Skills: Holes Skill

Narya interactive proof development with typed holes

UncategorizedID: plurigrid/asi/holes

Install this agent skill to your local

pnpm dlx add-skill https://github.com/plurigrid/asi/tree/HEAD/plugins/asi/skills/holes

Skill Files

Browse the full folder contents for holes.

Download Skill

Loading file tree…

plugins/asi/skills/holes/SKILL.md

Skill Metadata

Name
holes
Description
Narya interactive proof development with typed holes

Holes Skill

Interactive proof development using typed holes in Narya proof assistant.

See HOLES_GUIDE.md for detailed usage.

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

  • general: 734 citations in bib.duckdb

Cat# Integration

This skill maps to Cat# = Comod(P) as a bicomodule:

Trit: 0 (ERGODIC - bridge/coordinator)
Home: Prof (profunctors/bimodules)
Poly Op: ⊗ (parallel composition)
Kan Role: Adj (adjunction bridge)

GF(3) Naturality

Typed holes represent "gaps" in the proof space - they are ERGODIC elements that bridge between what is known (MINUS) and what needs to be constructed (PLUS).