@@ -11,9 +11,19 @@ infixr 3 &&&
11class Category arr => Arrow (arr : Type -> Type -> Type) where
11class Category arr => Arrow (arr : Type -> Type -> Type) where
12 arrow : (a -> b) -> arr a b
12 arrow : (a -> b) -> arr a b
13 first : arr a b -> arr (a, c) (b, c)
13 first : arr a b -> arr (a, c) (b, c)
14 second : arr a b -> arr (c, a) (c, b)
15 second : arr a b -> arr (c, a) (c, b)
16+ second f = arrow swap >>> first f >>> arrow swap where
17+ swap : (x,y) -> (y,x)
15 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
20 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
21+ f *** g = first f >>> second g
16 (&&&) : arr a b -> arr a b' -> arr a (b, b')
23 (&&&) : arr a b -> arr a b' -> arr a (b, b')
24+ f &&& g = arrow dup >>> f *** g where
18instance Arrow Morphism where
28instance Arrow Morphism where
19 arrow f = Mor f
29 arrow f = Mor f