From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 18:19:11 +0000 (+0200)
Subject: Refactoring of examples
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=331fb6f79a56dc2141892f891c2275cbe42f6576;p=cubicaltt.git

Refactoring of examples
---

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index 9db5b1d..81a71d9 100644
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -2,18 +2,6 @@ module hedberg where
 
 import prelude
 
-const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)
-
-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))
-
-exConst (A : U) : U = (f:A -> A) * const A f
-
-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))
-
 hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :
   (b : A) (p : Id A a b) ->
             Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =
diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index f0f760b..eae59df 100644
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -2,17 +2,6 @@ module newhedberg where
 
 import prelude
 
-const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)
-
-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))
-
-exConst (A : U) : U = (f:A -> A) * const A f
-
-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))
-
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = 
  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)))
diff --git a/examples/other.ctt b/examples/other.ctt
index f90c3fe..9ee32bf 100644
--- 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 1bfd968..f2b8f0c 100644
--- 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 33c8160..0eacacd 100644
--- 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