Directed Yoneda Skill

yoneda-directed

Directed Yoneda lemma as directed path induction. Riehl-Shulman's key insight for synthetic ∞-categories.

plurigrid/asi·0installs67stars

SKILL.md

Full skill instructions

Directed Yoneda Skill

"The dependent Yoneda lemma is a directed analogue of path induction." — Emily Riehl & Michael Shulman

The Key Insight

Standard HoTT	Directed HoTT
Path induction	Directed path induction
Yoneda for ∞-groupoids	Dependent Yoneda for ∞-categories
Types have identity	Segal types have composition

Core Definition (Rzk)

#lang rzk-1

-- Dependent Yoneda lemma
-- To prove P(x, f) for all x : A and f : hom A a x,
-- it suffices to prove P(a, id_a)

#define dep-yoneda
  (A : Segal-type) (a : A)
  (P : (x : A) → hom A a x → U)
  (base : P a (id a))
  : (x : A) → (f : hom A a x) → P x f
  := λ x f. transport-along-hom P f base

-- This is "directed path induction"
#define directed-path-induction := dep-yoneda

Chemputer Semantics

Chemical Interpretation:

To prove a property of all reaction products from starting material A,
It suffices to prove it for A itself (the identity "null reaction")
Directed induction propagates the property along all reaction pathways

GF(3) Triad

yoneda-directed (-1) ⊗ elements-infinity-cats (0) ⊗ synthetic-adjunctions (+1) = 0 ✓
yoneda-directed (-1) ⊗ cognitive-superposition (0) ⊗ curiosity-driven (+1) = 0 ✓

As Validator (-1), yoneda-directed verifies:

Properties propagate correctly along morphisms
Base case at identity suffices
Induction principle is sound

Theorem

For any Segal type A, element a : A, and type family P,
if we have base : P(a, id_a), then for all x : A and f : hom(a, x),
we get P(x, f).

This is analogous to:
"To prove ∀ paths from a, prove for the reflexivity path"

References

Riehl, E. & Shulman, M. (2017). "A type theory for synthetic ∞-categories." §5.
Rzk sHoTT library

Install skill

Copy and run in your terminal

npx -y skills add https://github.com/plurigrid/asi --skill yoneda-directed

View on GitHub

ies/music-topos/.codex/skills/yoneda-directed/SKILL.md

modern-python
Modern Python best practices. Use when creating new Python projects, and writing Python scripts, or migrating existing projects from legacy tools.
1 installs
ghostty
Control Ghostty terminal emulator via CLI. Manage windows, tabs, splits, and configuration.
0 installs
gay-integration
Gay.jl integration for bisimulation games with proper hue-based trit derivation and GF(3) conservation
0 installs
wev-verification
WEV Verification Skill
0 installs

More skills from plurigrid

plurigrid/asi

cargo

Rust package manager (36 subcommands).

67 0

View

plurigrid/asi

Translate Figma nodes into production-ready code with 1:1 visual fidelity using the Figma MCP workflow (design context, screenshots, assets, and project-convention translation). Trigger when the user provides Figma URLs or node IDs, or asks to implement designs or components that must match Figma...

67 0

View

plurigrid/asi

StringZilla Operations: 'strings' Skill for Plurigrid ASI

**Status**: 🌳 Production Ready (upstream in StringZilla v3+) **Type**: High-Performance String Operations / SIMD-Accelerated Text Processing **Principle**: Zero-copy views, SIMD/SWAR acceleration, deterministic hashing **Frame**: Cross-language interoperability (C, C++, Python, Rust, Go, Swift, ...

67 0

View

plurigrid/asi

conformal-ga

Conformal Geometric Algebra (CGA) for circles, spheres, and Möbius transformations

67 0

View

plurigrid/asi

spec-to-code-compliance

Verifies code implements exactly what documentation specifies for blockchain audits. Use when comparing code against whitepapers, finding gaps between specs and implementation, or performing compliance checks for protocol implementations.

67 0

View

plurigrid/asi

zig-systems

Systems programming and performance optimization using Zig. Provides low-level abstractions, memory-safe compiled code, and performance benchmarking. Use for system-level operations, optimization, and interoperability with C/POSIX APIs.

67 0

View

plurigrid/asi

paypal-mcp

PayPal MCP server integration for invoices, payments, subscriptions, disputes, and transaction reporting via @paypal/mcp.

67 0

View

plurigrid/asi

unison

Unison language - content-addressed functional programming with abilities for effects, distributed computing, and structural types. Use for pure functional code, effect management, distributed systems, and refactoring-safe codebases.

67 0

View

plurigrid/asi

tasks-acset

Google Tasks management via TasksACSet. Transforms task operations into GF(3)-typed Interactions, routes to triadic queues, detects saturation for task-zero-as-condensed-state.

67 0

View

plurigrid/asi

c

World C Skill

67 0

View

plurigrid/asi

syrup

Syrup binary serialization for OCapN/CapTP wire format. Canonical encoding for capability messages.

67 0

View

plurigrid/asi

skill-installer

Install Codex skills into $CODEX_HOME/skills from a curated list or a GitHub repo path. Use when a user asks to list installable skills, install a curated skill, or install a skill from another repo (including private repos).

67 0

View