From: coquand Date: Thu, 30 Apr 2015 12:01:17 +0000 (+0200) Subject: updated collection X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9d3aa0f61af6d00ef276540b094e113b696fe992;p=cubicaltt.git updated collection --- diff --git a/examples/collection.ctt b/examples/collection.ctt index 3ebb7d3..606b269 100644 --- 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)