Fix bug in gensym and add Square

diff --git a/Connections.hs b/Connections.hs
index ce52a5bad70852f4de714e325b17aaecea3882ad..9d6fea15f14627c40a970df53470c199a349a0bb 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -230,9 +230,10 @@ propInvFormulaIncomp phi b = incomparables (invFormula phi b)
 
 -- | Nominal
 gensym :: [Name] -> Name
-gensym [] = Name "?0"
-gensym xs = Name ('?' : show (max+1))
-  where max = maximum [ read x | Name ('?':x) <- xs ]
+gensym xs = Name ('?' : show max)
+  where max = maximum' [ read x | Name ('?':x) <- xs ]
+        maximum' [] = 0
+        maximum' xs = maximum xs + 1
 
 gensyms :: [Name] -> [Name]
 gensyms d = let x = gensym d in x : gensyms (x : d)

diff --git a/examples/nat.ctt b/examples/nat.ctt
index ebd1af35590f5500eb00b7bb4db646c03d8c9051..73357f64e4b656c2d60412dec4873b0d28ec3ef8 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -80,14 +80,14 @@ compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b =
 
 compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
   <i> comp A (p @ i) [ (i = 1) -> q ]
-  
+
 kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
                           (r : Id A b d) : Id A c d =
   <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
 
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
--- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) 
+-- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
 --          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
 --   <j> <k> comp A a [ (j = 0) -> ... ]
 
@@ -98,3 +98,24 @@ inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 --                         (k ~> 0,p @@ i),
 --                         (k ~> 1,(s @@ j) @@ i)]
 
+
+
+--         u
+--    a0 ----- a1
+--    |        |
+-- r0 |        | r1
+--    |        |
+--    b0 ----- b1
+--         v
+
+Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
+               (b0 b1 : A) (v : Id A b0 b1)
+               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
+  = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
+
+testSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p =
+  <i> <j> comp A a
+     [(i = 0) -> <k> p @ (j \/ - k),
+      (i = 1) -> <k> p @ (j /\ k),
+      (j = 0) -> <k> p @ (i \/ - k),
+      (j = 1) -> <k> p @ (i /\ k)]
\ No newline at end of file