From: coquand <coquand@chalmers.se>
Date: Tue, 28 Apr 2015 11:22:26 +0000 (+0200)
Subject: added pi1s2
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7a00fd0e55433730b18cfb6a02863d3d45e31f38;p=cubicaltt.git

added pi1s2
---

diff --git a/Eval.hs b/Eval.hs
index 882c58c..3f2b1b8 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -222,9 +222,13 @@ app u v = case (u,v) of
 
 fstVal, sndVal :: Val -> Val
 fstVal (VPair a b)     = a
+fstVal (VElimComp _ _ u) = fstVal u
+fstVal (VCompElem _ _ u _) = fstVal u
 fstVal u | isNeutral u = VFst u
 fstVal u               = error $ "fstVal: " ++ show u ++ " is not neutral."
 sndVal (VPair a b)     = b
+sndVal (VElimComp _ _ u) = sndVal u
+sndVal (VCompElem _ _ u _) = sndVal u
 sndVal u | isNeutral u = VSnd u
 sndVal u               = error $ "sndVal: " ++ show u ++ " is not neutral."
 
diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt
new file mode 100644
index 0000000..0171f22
--- /dev/null
+++ b/examples/pi1S2.ctt
@@ -0,0 +1,25 @@
+module pi1S2 where
+
+import truncS2
+import groupoidTrunc
+
+lemGrp4 (X : U) (gX:groupoid X) : Id U (gTrunc S2 -> X) X
+ = compId U (gTrunc S2 -> X) (S2 -> X) X (univG S2 X gX) (lemGrp3 X gX)
+
+corr : Id U (gTrunc S2 -> gTrunc S2) (gTrunc S2) = lemGrp4 (gTrunc S2) (gTr S2)
+
+lemTransport (A :U) : 
+  (B : U) (p : Id U A B) (a0 a1 : A) -> Id B (transport p a0) (transport p a1) -> Id A a0 a1 =
+ J U A ( \ (B : U) (p : Id U A B) -> (a0 a1 : A) -> Id B (transport p a0) (transport p a1) -> Id A a0 a1) rem
+ where rem (a0 a1:A) (h:Id A a0 a1) : Id A a0 a1 = h
+
+corr1 : Id (gTrunc S2 -> gTrunc S2) (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) =
+ lemTransport (gTrunc S2 -> gTrunc S2) (gTrunc S2) corr 
+              (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) (refl (gTrunc S2) (inc north))
+
+corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = <i> corr1@i x 
+
+test : Id (gTrunc S2) (inc south) (inc north) = corr2 (inc south)
+
+test1 : Id (gTrunc S2) (inc north) (inc north) = corr2 (inc north)
+
diff --git a/examples/truncS2.ctt b/examples/truncS2.ctt
index 980b970..6349b8c 100644
--- a/examples/truncS2.ctt
+++ b/examples/truncS2.ctt
@@ -34,3 +34,5 @@ lemGrp2 (X : U) (gX:groupoid X) : Id U (suspOf S1 X) X =
 
 lemGrp3 (X : U) (gX: groupoid X) : Id U (S2 -> X) X =
  compId U (S2 -> X) (suspOf S1 X) X (funSusp S1 X) (lemGrp2 X gX)
+
+test (X:U) (gX: groupoid X) (f:S2 -> X) : X = transport (lemGrp3 X gX) f
\ No newline at end of file