Back to Details

yoneda-directed

Compare original and translation side by side

🇺🇸

Original

English
🇨🇳

Translation

Chinese

Directed Yoneda Skill

有向Yoneda Skill

"The dependent Yoneda lemma is a directed analogue of path induction." — Emily Riehl & Michael Shulman
"依赖Yoneda引理是路径归纳的有向类比。" — Emily Riehl & Michael Shulman

The Key Insight

核心见解

Standard HoTTDirected HoTT
Path inductionDirected path induction
Yoneda for ∞-groupoidsDependent Yoneda for ∞-categories
Types have identitySegal types have composition
标准HoTT有向HoTT
路径归纳有向路径归纳
适用于∞-群胚的Yoneda引理适用于∞-范畴的依赖Yoneda引理
类型具有恒等性Segal类型具有复合性

Core Definition (Rzk)

核心定义（Rzk）

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
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

Chemputer语义

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
化学解释:
  • 要证明从起始材料A得到的所有反应产物的某一性质，
  • 只需证明A本身满足该性质（即恒等「零反应」）
  • 有向归纳会沿着所有反应路径传播该性质

GF(3) Triad

GF(3)三元组

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
yoneda-directed (-1) ⊗ elements-infinity-cats (0) ⊗ synthetic-adjunctions (+1) = 0 ✓
yoneda-directed (-1) ⊗ cognitive-superposition (0) ⊗ curiosity-driven (+1) = 0 ✓
作为验证器(-1)，有向Yoneda可验证：
  • 性质沿态射正确传播
  • 恒等处的基例足够
  • 归纳原理是可靠的

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"
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

参考文献

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