Refactoring of examples

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index 9db5b1d9bc954088b288090b2e5396393656f829..81a71d95fa86302b533c1e2189512cad290700e1 100644 (file)
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -2,18 +2,6 @@ module hedberg where
 \r
 import prelude\r
 \r
-const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)\r
-\r
-decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split\r
-  inl a -> inl (f a)\r
-  inr h -> inr (\ (b:B) -> h (g b))\r
-\r
-exConst (A : U) : U = (f:A -> A) * const A f\r
-\r
-decConst (A : U) : dec A -> exConst A = split\r
-  inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)\r
-  inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))\r
-\r
 hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :\r
   (b : A) (p : Id A a b) ->\r
             Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =\r

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index f0f760b389b18cc6e3bd4f5bf2ba1c81493af071..eae59dfa97965d9fadc98e917ae814d8e3ebf59d 100644 (file)
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -2,17 +2,6 @@ module newhedberg where
 \r
 import prelude\r
 \r
-const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)\r
-\r
-decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split\r
-  inl a -> inl (f a)\r
-  inr h -> inr (\ (b:B) -> h (g b))\r
-\r
-exConst (A : U) : U = (f:A -> A) * const A f\r
-\r
-stableConst (A : U) (sA: stable A) : exConst A = \r
- (\ (x:A) -> sA (dNeg A x),\ (x y:A) -> <i>sA (propNeg (neg A) (dNeg A x) (dNeg A y) @ i))\r
-\r
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = \r
  transport (<i>Square A a a (refl A a) a (p@i) (<j>p@i/\j) (f a (refl A a)) (f (p@i) (<j>p@i/\j)))\r

diff --git a/examples/other.ctt b/examples/other.ctt
index f90c3fe50bb00f1977d19abe468b561974312655..9ee32bf07bfcdb0645a2e0ee5b132f452dffcf3d 100644 (file)
--- a/examples/other.ctt
+++ b/examples/other.ctt
@@ -2,12 +2,6 @@ module other where
 
 import retract
 
-propUnit : prop Unit = rem
- where rem1 : (x:Unit) -> Id Unit x tt = split tt -> refl Unit tt
-       rem (x:Unit) : (y:Unit) -> Id Unit x y = split tt -> rem1 x
-
-setUnit : set Unit = propSet Unit propUnit
-
 propSingl (A:U) (a:A) (u v : singl A a) : Id (singl A a) u v =
  compId (singl A a) u (a,refl A a) v (<i>(contrSingl A a u.1 u.2)@-i) (contrSingl A a v.1 v.2)
 

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 1bfd96882fe6a80e180b824623bc3d09adb718f3..f2b8f0cd1a861d7ef1aba24f11e89121ebe58d03 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -143,17 +143,45 @@ neg (A : U) : U = A -> N0
 
 data Unit = tt
 
+propUnit : prop Unit = rem
+ where rem1 : (x:Unit) -> Id Unit x tt = split tt -> refl Unit tt
+       rem (x:Unit) : (y:Unit) -> Id Unit x y = split tt -> rem1 x
+
+setUnit : set Unit = propSet Unit propUnit
+
 data or (A B : U) = inl (a : A)
                   | inr (b : B)
 
 stable (A:U) : U = neg (neg A) -> A
 
+const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)
+
+exConst (A : U) : U = (f:A -> A) * const A f
+
+
+propN0 : prop N0 = \ (x y:N0) -> efq (Id N0 x y) x
+
+propNeg (A:U) : prop (neg A) = \ (f g:neg A) -> <i>\(x:A) -> (propN0 (f x) (g x))@i
+
+dNeg (A:U) (a:A) : neg (neg A) = \ (h : neg A) -> h a
+
 dec (A : U) : U = or A (neg A)
 
+decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split
+  inl a -> inl (f a)
+  inr h -> inr (\ (b:B) -> h (g b))
+
 decStable (A:U) : dec A -> stable A = split
  inl a -> \ (h :neg (neg A)) -> a
  inr b -> \ (h :neg (neg A)) -> efq A (h b)
 
+decConst (A : U) : dec A -> exConst A = split
+  inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)
+  inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))
+
+stableConst (A : U) (sA: stable A) : exConst A = 
+ (\ (x:A) -> sA (dNeg A x),\ (x y:A) -> <i>sA (propNeg (neg A) (dNeg A x) (dNeg A y) @ i))
+
 discrete (A : U) : U = (a b : A) -> dec (Id A a b)
 
 injective (A B : U) (f : A -> B) : U =

diff --git a/examples/testall.ctt b/examples/testall.ctt
index 33c8160a161f190e5c402f2b6a8f23aecb68a523..0eacacd0bc211b9f73290b2af00a36c6b6ec9129 100644 (file)
--- a/examples/testall.ctt
+++ b/examples/testall.ctt
@@ -6,12 +6,15 @@ import uafunext2
 import helix
 import susp
 import ex1
-import integer
 import setTrunc
-import newhedberg
 import prop
 import quotient
 import torus
 import s2
 import uafunext1
-import list
\ No newline at end of file
+import list
+import hedberg
+import newhedberg
+import other
+-- integer has to be after hedberg as it redefines neg
+import integer