Correct B

src/test.cccatt

@@ -33,13 +33,13 @@ coh K (a b : .) : a → b → a
 
 coh S (a b c : .) : (a → b → c) → (a → b) → a → c
 
-coh B (a b : .) : (a -> b) -> a -> b
-
 coh ap (a b : .) (t : a → b) (u : a) : b
 
 coh comp (a b c : .) (f : a → b) (g : b → c) : a → c
 
-coh comp' (a b c : .) : (a -> b) -> (b -> c) -> a -> c
+coh B (a b c : .) : (b -> c) -> (a -> b) -> a -> c
+
+coh B' (a b c : .) : (a -> b) -> (b -> c) -> a -> c
 
 coh W (a b : .) : (a -> a -> b) -> (a -> b)
 
@@ -79,10 +79,14 @@ coh ap-K (a b : .) (x : a) (y : b) : ap b a (ap a (b -> a) (K a b) x) y = x
 
 coh ap-comp (a b c : .) (f : a -> b) (g : b -> c) (x : a) : ap a c (comp a b c f g) x = ap b c g (ap a b f x)
 
-## Curry's identities
+## Curry's axioms
 
 coh ax3 (a b : .) : ap (a -> b -> b) ((a -> b) -> a -> b) (S a b b) (ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)) = I (a -> b)
 
+coh ax3 (a b : .) : ap (a -> b -> b) ((a -> b) -> a -> b) (S a b b) (ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)) = I (a -> b)
+
+# coh ax4 (a b c : .) : ap
+
 # # I is derivable
 # coh SKK (a : .) : ap _ _ (ap _ _ (S _ _ _) (K _ _)) (K _ _) = I a
 
@@ -104,7 +108,7 @@ let zero (a : .) : nat a := K' (a -> a) a
 
 let one (a : .) : nat a := I (a -> a)
 
-let two (a : .) : nat a := ap ((a -> a) -> (a -> a) -> (a -> a)) ((a -> a) -> (a -> a)) (W (a -> a) (a -> a)) (comp' a a a)
+let two (a : .) : nat a := ap ((a -> a) -> (a -> a) -> (a -> a)) ((a -> a) -> (a -> a)) (W (a -> a) (a -> a)) (B a a a)
 
 # let add (a : .) (m n : nat a) (f : a -> a) (x : a) := ap a a (ap (a -> a) (a -> a) m f) (ap a a (ap (a -> a) (a -> a) n f) x)