A formalisation of the logical equivalence of the Yoneda lemma and dependent path induciton

87d0e4e1
—
tslil
2 years ago

Updated to match UniMath names

2e35b003
—
tslil
2 years ago

Added description

2c93da3b
—
tslil clingman
4 years ago

Markdown formatting

- read-only
- https://git.sr.ht/~tslil/y_and_j
- read/write
- git@git.sr.ht:~tslil/y_and_j

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:

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