Here we prove that the Yoneda lemma and path induction are logically equivalent.
Our interpretation of the Yoneda lemma is from the perspective of ''types as ∞-groupoids''. More precisely, we view types A : UU as 'categories' with 'homs' A(a, b) := Id a b. This stance compels us to define 'presheaves' as the type A -> UU, and thus natural transformations as
∏ (a : A), F a -> G a.
The type corresponding to the Yoneda lemma,
yoneda_type, we take as comprising a function
y which takes elements of a presheaf
F a to natural transformations out of the representable
λ b, a = b to
F. We additionally hypothesise that
y itself is suitably natural in presheaves
F, and that it satisfies two computations:
λ b, a = bit sends
idpath ato a natural transformation whose component at
b : Asends a path
p : a = bto itself
F, evaluating the resulting natural transformation
(λ b, a = b) -> F bat
ayields the term
x : F awe began with
The type corresponding to path induction,
j_type, we take to be the standard formulation of dependent path induction.
j_type -> yoneda_type is straightforward and expected, but the present proof in the other direction has the curious feature of first constructing a non-computing path induction function, and then using that and Yoneda again, to derive a correctly computing term. All of this is done in the absence of function extensionality and Univalence.