From 87d0e4e1c618ce154b60e1713ea7d007ac5bcba3 Mon Sep 17 00:00:00 2001
From: tslil <>
Date: Thu, 30 Sep 2021 22:01:15 -0400
Subject: Updated to match UniMath names

---
 y_and_j.v | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'y_and_j.v')

diff --git a/y_and_j.v b/y_and_j.v
index cd2576f..4098050 100644
--- a/y_and_j.v
+++ b/y_and_j.v
@@ -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.
-- 
cgit v1.3.1