Asi narya-hatchery

Narya Hatchery

install

source · Clone the upstream repo

git clone https://github.com/plurigrid/asi

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/narya-hatchery" ~/.claude/skills/plurigrid-asi-narya-hatchery-0800b9 && rm -rf "$T"

manifest: skills/narya-hatchery/SKILL.md

source content

Narya Hatchery

name: narya-hatchery description: Higher-dimensional type theory proof assistant with observational Id/Bridge types, parametricity, and ProofGeneral integration. trit: 0 color: "#3A71C0"

Overview

Narya is a proof assistant implementing Multi-Modal, Multi-Directional, Higher/Parametric/Displayed Observational Type Theory.

Core Features

Normalization-by-evaluation algorithm and typechecker
Observational-style theory with Id/Bridge types satisfying parametricity
Variable arity and internality for bridge types
User-definable mixfix notations
Record types, inductive datatypes, coinductive codatatypes
Matching and comatching case trees
Import/export and separate compilation
Typed holes with later solving
ProofGeneral interaction mode

Type Theory Features

Bridge Types with Parametricity

-- Observational identity via bridges
bridge : (A : Type) → (x y : A) → Bridge x y → x ≡ y

Higher-Dimensional Structure

Narya supports higher-dimensional type theory where:

Types can have internal dimensions
Parametricity is built into the type theory
Bridge types generalize equality

Gay.jl Integration

# Initialize with Narya's chromatic seed
gay_seed!(0xbfe738ce2e1c5f1f)

# P3 extension gamut learning
function loss(params, seed, target_gamut=:p3_extension)
    color = forward_color(params, projection, seed)
    return out_of_gamut_distance(color, target_gamut)
end

Installation

# From source
git clone https://github.com/mikeshulman/narya
cd narya
dune build

Documentation

Repository

Source: TeglonLabs/narya (fork of mikeshulman/narya)
Seed:
```
0xbfe738ce2e1c5f1f
```
Index: 49/1055
Color: #d6621c

GF(3) Triad

proofgeneral-narya (-1) ⊗ narya-hatchery (0) ⊗ gay-mcp (+1) = 0 ✓

Related Skills

```
proofgeneral-narya
```
- Emacs integration
```
holes
```
- Interactive proof development
```
move-narya-bridge
```
- Move contract verification

SDF Interleaving

This skill connects to Software Design for Flexibility (Hanson & Sussman, 2021):

Primary Chapter: 5. Evaluation

Concepts: eval, apply, interpreter, environment

GF(3) Balanced Triad

narya-hatchery (−) + SDF.Ch5 (−) + [balancer] (−) = 0

Skill Trit: -1 (MINUS - verification)

Secondary Chapters

Ch4: Pattern Matching
Ch6: Layering

Connection Pattern

Evaluation interprets expressions. This skill processes or generates evaluable forms.