#A proof of Yoneda <-> Dependent path induction formalised in UniMath

Formalisation: y_and_j.v

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:

1. on the representable presheaf λ b, a = b it sends idpath a to a natural transformation whose component at b : A sends a path p : a = b to itself
2. at a generic presheaf F, evaluating the resulting natural transformation (λ b, a = b) -> F b at a yields the term x : F a we began with

The type corresponding to path induction, j_type, we take to be the standard formulation of dependent path induction.

The direction 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.