holes skill

safe

This skill helps you develop interactive proofs using typed holes in the Narya proof assistant, guiding gap filling and proof construction.

npx playbooks add skill plurigrid/asi --skill holes

Review the files below or copy the command above to add this skill to your agents.

Files (3)

SKILL.md

754 B

---
name: holes
description: Narya interactive proof development with typed holes
trit: 0
color: "#26D826"
catsharp:
  home: Prof
  poly_op: ⊗ (parallel)
  kan_role: Adj
  bicomodule: true
---

# Holes Skill

Interactive proof development using typed holes in Narya proof assistant.

See [HOLES_GUIDE.md](./HOLES_GUIDE.md) for detailed usage.

## 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).

Overview

This skill provides interactive proof development in the Narya proof assistant using typed holes as first-class proof objects. It treats holes as typed placeholders that guide construction, exploration, and composition of partial proofs. The interface emphasizes modular composition and explicit bridges between known lemmas and goals.

How this skill works

Typed holes act as named, typed gaps in a proof term; the assistant tracks their expected types and dependencies and exposes them for incremental filling. The system represents module interactions as bicomodule-like structures that coordinate composition, parallel composition, and adjunction-style bridges between contexts. Users iteratively refine holes, inspect constraints, and plug constructed terms to discharge goals and propagate changes.

When to use it

When building complex proofs incrementally and managing many interdependent subgoals.
When you need explicit placeholders to reason about partially constructed terms.
When composing proofs across different contexts or modules that require coordinating bridges.
For exploratory proof search where constraints guide synthesis of missing pieces.
When teaching or debugging proof strategies and wanting visible, typed gaps.

Best practices

Name holes descriptively to document intent and expected behavior.
Keep hole types as precise as possible to reduce search space and improve suggestions.
Use small composable holes rather than large amorphous placeholders to simplify filling.
Review dependency graphs to avoid circular expectations between holes.
Leverage module composition primitives to reuse constructions and reduce duplication.

Example use cases

Incrementally constructing a long derivation by exposing intermediate typed holes for each lemma.
Coordinating proofs across two adjacent contexts where an adjunction-like bridge transports structure.
Teaching proof tactics by leaving illustrative holes that students must fill with correct terms.
Rapid prototyping of categorical constructions where bicomodule-style composition clarifies interfaces.
Constrained synthesis: use hole types to drive automated suggestion engines toward valid completions.

FAQ

What is a typed hole?

A typed hole is a named placeholder carrying an expected type; it indicates a missing subterm and constrains possible fillings.

How does composition between contexts work?

Composition uses compositional primitives resembling bimodules and adjunction bridges to transport and combine partial constructions across contexts.