diff options
| author | tslil <> | 2021-09-30 19:31:49 -0400 |
|---|---|---|
| committer | tslil <> | 2021-09-30 19:38:15 -0400 |
| commit | 2e35b0033b994c6360ceb48161b6da3674934a73 (patch) | |
| tree | 7f0a3661f0b91a084a6a1a4b9517f52c2637a2fc /y_and_j.v | |
| parent | 2c93da3be2a88c222efda21efa783b124c77f9f9 (diff) | |
Added description
Diffstat (limited to 'y_and_j.v')
| -rw-r--r-- | y_and_j.v | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -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 |