From: Anders Date: Fri, 20 Mar 2015 09:30:07 +0000 (+0100) Subject: Fix bug in gensym and add Square X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0f0cae07f753656d0e81e8dbc8a8720be2cab825;p=cubicaltt.git Fix bug in gensym and add Square --- diff --git a/Connections.hs b/Connections.hs index ce52a5b..9d6fea1 100644 --- 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 ebd1af3..73357f6 100644 --- 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 = 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 = 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 = 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' = -- comp A a [ (j = 0) -> ... ] @@ -98,3 +98,24 @@ inv (A : U) (a b : A) (p : Id A a b) : Id A b a = 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 ( (IdP ( 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 = + comp A a + [(i = 0) -> p @ (j \/ - k), + (i = 1) -> p @ (j /\ k), + (j = 0) -> p @ (i \/ - k), + (j = 1) -> p @ (i /\ k)] \ No newline at end of file