updated collection

diff --git a/examples/collection.ctt b/examples/collection.ctt
index 3ebb7d3ba35275e808980e3eccff02ba53b6a198..606b26911ac6a803bd8fd4a89ff2052dc312644c 100644 (file)
--- a/examples/collection.ctt
+++ b/examples/collection.ctt
@@ -5,18 +5,18 @@ import pi
 import univalence
 import retract
 
-lem1 (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB)
+setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB)
 
-lem2 (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB)
+groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB)
 
 lem3 (A B : U) (t u : Equiv A B) : Id U (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1)
  = lemSigProp (A->B) (isEquiv A B) (propIsEquiv A B) t u 
 
 lem4 (A B : U) (sB:set B) (t u:Equiv A B) : prop (Id  (Equiv A B) t u)
- = substInv U prop (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (lem1 A B sB t.1 u.1)
+ = substInv U prop (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (setFun A B sB t.1 u.1)
 
 lem5 (A B : U) (gB:groupoid B) (t u:Equiv A B) : set (Id (Equiv A B) t u)
- = substInv U set  (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (lem2 A B gB t.1 u.1)
+ = substInv U set  (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1)
 
 lem6 (A B : U) (sB : set B) : set (Id U A B) = 
  retractSet (Id U A B) (Equiv A B) (IdToEquiv A B) (EquivToId A B) (secIdEquiv A B) (lem4 A B sB)