diff options
| -rw-r--r-- | README.md | 14 | ||||
| -rw-r--r-- | y_and_j.v | 3 |
2 files changed, 14 insertions, 3 deletions
@@ -1,5 +1,15 @@ # A proof of Yoneda <-> Dependent path induction formalised in UniMath -Write-up: pending +Formalisation: [y\_and\_j.v](y_and_j.v) -Formalisation: [y_and_j.v](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. @@ -1,3 +1,4 @@ +(* For function extensionality for use in a corollary *) Require Import UniMath.Foundations.UnivalenceAxiom. Definition j_type @@ -231,7 +232,7 @@ Print All Dependencies y_derive_j. Print All Dependencies j_derive_y. -(** This proof makes use of function extensionality twice. +(** The following proof makes use of function extensionality twice. Notice however that it is _not_ used to derive a term of type [yoneda_type]. With [j_derive_y] alone we may construct |