diff options
| -rw-r--r-- | y_and_j.v | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -1,5 +1,4 @@ -(* For function extensionality for use in a corollary *) -Require Import UniMath.Foundations.UnivalenceAxiom. +Require Import UniMath.Foundations.PartA. Definition j_type := ∑ (j : ∏ (A : UU) (a : A) (D : ∏ (b : A), a = b -> UU), @@ -99,9 +98,9 @@ Section j_to_yoneda. Definition j_derive_y : yoneda_type. exists j_yoneda_fun. - apply dirprodpair. + apply make_dirprod. - exact j_yoneda_naturality. - - apply dirprodpair. + - apply make_dirprod. + exact j_yoneda_special. + exact (λ A F a x, j_derive_idtohomot (j_yoneda_fromto A F a) x). Defined. @@ -241,15 +240,19 @@ Print All Dependencies j_derive_y. That is, in the presence of function extensionality, [yoneda_type] implies a Yoneda equivalence. *) + +(* For function extensionality *) +Require Import UniMath.Foundations.UnivalenceAxiom. + Definition yoneda_tofrom (j : j_type) (A : UU) (F : A -> UU) (a : A) (α : nat_trans (λ b, a = b) F) : - j_yoneda_fun A F a (j_yoneda_from A F a α) = α. + j_yoneda_fun j A F a (j_yoneda_from A F a α) = α. Proof. apply isweqtoforallpaths ; intro b. apply funextfun ; intro p. apply ((pr1 j) A a (λ b p, - j_yoneda_fun A F a (j_yoneda_from A F a α) b p = α b p)). + j_yoneda_fun j A F a (j_yoneda_from A F a α) b p = α b p)). unfold j_yoneda_fun. - rewrite (pr2 (j_derive_transport F) a). + rewrite (pr2 (j_derive_transport j F) a). apply idpath. Defined. |