Directed Yoneda Skill 围绕“有向米田引理即是有向路径归纳”这一核心洞察展开。
核心洞察
该技能引用 Emily Riehl 与 Michael Shulman 的表述：“依赖米田引理是路径归纳的有向类比。”资料以对照方式区分了标准 HoTT 与有向 HoTT：
- 标准 HoTT 使用路径归纳（path induction）；有向 HoTT 使用有向路径归纳（directed path induction）。
- 标准 HoTT 针对 ∞-群胚的米田引理；有向 HoTT 针对 ∞-范畴的依赖米田引理。
- 标准 HoTT 中类型具有同一性（identity）；有向 HoTT 中 Segal 类型具有复合（composition）。
核心定义（Rzk）
资料使用 Rzk 语言（#lang rzk-1）给出依赖米田引理的定义：要证明对所有 x : A 和 f : hom A a x 成立的性质 P(x, f)，只需证明 P(a, id_a)。其形式化表达为：
#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
即：directed-path-induction 被直接定义为 dep-yoneda。
定理
对于任意 Segal 类型 A、元素 a : A 以及类型族 P，如果拥有 base : P(a, id_a)，那么对所有 x : A 和 f : hom(a, x)，都可以得到 P(x, f)。资料将其类比为：“要证明从 a 出发的所有路径，只需为自反路径作证明。”
Chemputer 语义
资料给出化学解释：要证明从起始材料 A 出发的所有反应产物的某个性质，只需对 A 本身（即同一“零反应”）证明该性质；有向归纳会将这一性质沿所有反应路径传播。
GF(3) 三元组
该技能被标注为验证器（Validator，-1 极性），并给出两个满足 GF(3) 守恒的三元组关系：
yoneda-directed (-1) ⊗ elements-infinity-cats (0) ⊗ synthetic-adjunctions (+1) = 0 ✓ yoneda-directed (-1) ⊗ cognitive-superposition (0) ⊗ curiosity-driven (+1) = 0 ✓
作为验证器（-1），yoneda-directed 验证：性质沿态射正确传播、单位元处的基例足够、归纳原理是可靠的。
适用场景与限制
从资料看，该技能主要用于合成 ∞-范畴与有向同伦类型论的形式化推理，充当验证器角色。其定理与代码示例均针对 Segal 类型与 Rzk 语言环境。资料未说明该技能的具体调用方式、安装命令、接口、运行环境要求、性能表现或收费信息，这些内容暂未提供。