@@ -11,9 +11,19 @@ infixr 3 &&&
1111class Category arr => Arrow (arr : Type -> Type -> Type) where
1212 arrow : (a -> b) -> arr a b
1313 first : arr a b -> arr (a, c) (b, c)
14+
1415 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)
18+ swap (x,y) = (y,x)
19+
1520 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
21+ f *** g = first f >>> second g
22+
1623 (&&&) : arr a b -> arr a b' -> arr a (b, b')
24+ f &&& g = arrow dup >>> f *** g where
25+ dup : x -> (x,x)
26+ dup x = (x,x)
1727
1828instance Arrow Morphism where
1929 arrow f = Mor f