From 2e35b0033b994c6360ceb48161b6da3674934a73 Mon Sep 17 00:00:00 2001
From: tslil <>
Date: Thu, 30 Sep 2021 19:31:49 -0400
Subject: Added description

---
 y_and_j.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'y_and_j.v')

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