diff options
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 |