yoneda-directed
Installation
SKILL.md
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