added pi1s2

diff --git a/Eval.hs b/Eval.hs
index 882c58c33db3e65aec2e00a4d092472a4e951830..3f2b1b84e0f7fc24c129e3bff771f6233dab16a8 100644 (file)
--- 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 (file)
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 980b970152c7de6651690c53ec463ce5c73d915f..6349b8cef207cd27878375425c2618a2bd1cde25 100644 (file)
--- 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