0 | ||| This module defines the product of two categories.
 1 | module Control.Category.Instances.Prod
 2 |
 3 | import Control.Category
 4 | import Control.Category.Records
 5 | import Data.Morphisms
 6 |
 7 | %default total
 8 |
 9 | ||| The product category of two other categories.
10 | public export
11 | record Prod (cat : a -> b -> Type) (cat' : a' -> b' -> Type)
12 |             (x : (a, a')) (y : (b, b')) where
13 |   constructor MkProd
14 |   fst : cat (fst x) (fst y)
15 |   snd : cat' (snd x) (snd y)
16 |
17 |
18 | ------------------------------------------------------------
19 | -- Interface Style
20 | ------------------------------------------------------------
21 |
22 | public export
23 | Semigroupoid cat => Semigroupoid cat' => Semigroupoid (Prod cat cat') where
24 |   MkProd f f' . MkProd g g' = MkProd (f . g) (f' . g')
25 |
26 | public export
27 | Category cat => Category cat' => Category (Prod cat cat') where
28 |   id = MkProd id id
29 |   MkProd f f' . MkProd g g' = MkProd (f . g) (f' . g')
30 |
31 |
32 | -- Functor/Bifunctor equivalence
33 | -- Unfortunately, we can't make any of these resolve automatically
34 | -- due to the use of `curry`/`uncurry`
35 |
36 | namespace CatFunctor
37 |   public export
38 |   [FromCatBifunctor] CatBifunctor catA catB cat' f => CatFunctor (Prod catA catB) cat' (uncurry f) where
39 |     map {a=(_,_),b=(_,_)} (MkProd f g) = bimap f g
40 |
41 |   public export
42 |   [FromBifunctor] Bifunctor f => CatFunctor (Prod Morphism Morphism) Morphism (uncurry f) where
43 |     map {a=(_,_),b=(_,_)} (MkProd (Mor f) (Mor g)) = Mor (bimap f g)
44 |
45 |   public export
46 |   [FromBifunctor'] Bifunctor f => CatFunctor (Prod (~~>) (~~>)) (~~>) (uncurry f) where
47 |     map {a=(_,_),b=(_,_)} (MkProd f g) = Prelude.bimap f g
48 |
49 | namespace CatBifunctor
50 |   public export
51 |   [FromCatFunctor] CatFunctor (Prod catA catB) cat' f => CatBifunctor catA catB cat' (curry f) where
52 |     bimap f' g = map {cat=Prod catA catB,f} (MkProd f' g)
53 |
54 | public export
55 | [Horizontal] CatFunctor catF catF' f => CatFunctor catG catG' g =>
56 |     CatFunctor (Prod catF catG) (Prod catF' catG') (Prelude.bimap f g) where
57 |   map {a=(_,_),b=(_,_)} (MkProd f g) = MkProd (map f) (map g)
58 |
59 |
60 | ------------------------------------------------------------
61 | -- Record Style
62 | ------------------------------------------------------------
63 |
64 | namespace SemigroupoidR
65 |   public export
66 |   Prod : (cat,cat' : SemigroupoidR) -> SemigroupoidR
67 |   Prod (MkSemigroupoidR cat) (MkSemigroupoidR cat') = MkSemigroupoidR (Prod cat cat')
68 |
69 | namespace CategoryR
70 |   public export
71 |   Prod : (cat,cat' : CategoryR) -> CategoryR
72 |   Prod (MkCategoryR cat) (MkCategoryR cat') = MkCategoryR (Prod cat cat')
73 |
74 | public export
75 | FunctorProd : (f : FunctorR catF catF') -> (g : FunctorR catG catG') ->
76 |               FunctorR (Prod catF catG) (Prod catF' catG')
77 | FunctorProd {catF=MkCategoryR {},catF'=MkCategoryR {},catG=MkCategoryR {},catG'=MkCategoryR {}}
78 |   (MkFunctorR f) (MkFunctorR g) = MkFunctorR (bimap f g) {impl = Horizontal}
79 |