0 | module Control.Category
 1 |
 2 | import Data.Morphisms
 3 |
 4 |
 5 | public export
 6 | interface Category (m : o -> o -> Type) where
 7 |   identity : (a : o) -> m a a
 8 |   cmp : m b c -> m a b -> m a c
 9 |
10 | export
11 | Category Morphism where
12 |   identity a = Mor id
13 |   cmp (Mor g) (Mor f) = Mor (g . f)
14 |
15 | public export
16 | record Op (m : o -> o -> Type) (a : o) (b : o) where
17 |   constructor MkOp
18 |   getOp : m b a
19 |
20 | {-
21 | Category m => Category (Op m) where
22 |   identity = MkOp . identity
23 |   cmp (MkOp f) (MkOp g) = MkOp (cmp g f)
24 | -}
25 |
26 | public export
27 | data ProdC : (m1 : o1 -> o1 -> Type) -> (m2 : o2 -> o2 -> Type) -> (o1,o2) -> (o1,o2) -> Type where
28 |   MkProdC : {0 a1 : o1} -> {0 b1 : o1} -> {0 a2 : o2} -> {0 b2 : o2} -> m1 a1 b1 -> m2 a2 b2 -> ProdC m1 m2 (a1,a2) (b1,b2)
29 |
30 | proj1C : ProdC m1 m2 (a1,a2) (b1,b2) -> m1 a1 b1
31 | proj1C (MkProdC f _) = f
32 |
33 | proj2C : ProdC m1 m2 (a1,a2) (b1,b2) -> m2 a2 b2
34 | proj2C (MkProdC _ f) = f
35 |
36 | {-
37 | (Category m1, Category m2) => Category (ProdC m1 m2) where
38 |   identity (x,y) = MkProdC (identity x) (identity y)
39 |   cmp (MkProdC g1 g2) (MkProdC f1 f2) = MkProdC (cmp g1 f1) (cmp g2 f2)
40 | -}
41 |