0 | module Control.Category.Closed
 1 |
 2 | import Control.Category.Core
 3 | import Control.Category.Functor
 4 | import Control.Category.Monoidal
 5 | import Control.Category.Cartesian
 6 | import Data.Morphisms
 7 |
 8 | %default total
 9 |
10 | ------------------------------------------------------------
11 | -- Interface
12 | ------------------------------------------------------------
13 |
14 | ||| A monoidal category is *closed* if it can meaningfully represent
15 | ||| its morphisms as an object inside of itself. More specifically,
16 | ||| the internal hom ``(a `hom` b)`` is an object that encodes the
17 | ||| set of morphisms from `a` to `b`.
18 | |||
19 | ||| Formally, a monoidal category is closed if the functor
20 | ||| ``(`ten` a)`` has a right adjoint functor `hom a`.
21 | |||
22 | ||| This is the interface-style definition of a closed monoidal category.
23 | ||| For the record-style definition, see `Control.Category.Records.ClosedR`.
24 | |||
25 | ||| Laws:
26 | ||| * `curry` is natural in `a`,`b`,`c` (see `NatTrans`)
27 | ||| * `uncurry` is natural in `a`,`b`,`c` (see `NatTrans`)
28 | public export
29 | interface Monoidal cat ten i =>
30 |     Closed (0 cat : Hom obj) (ten,hom : obj -> obj -> obj) (i : obj) | cat,ten where
31 |   constructor MkClosed
32 |   ||| The currying transformation.
33 |   curry : {a,b,c : _} -> cat (a `ten` b) c -> cat a (b `hom` c)
34 |   ||| The uncurrying transformation.
35 |   uncurry : {a,b,c : _} -> cat a (b `hom` c) -> cat (a `ten` b) c
36 |
37 | ||| A monoidal category that is both cartesian and closed.
38 | |||
39 | ||| This is the interface-style definition of a cartesian closed
40 | ||| monoidal category. For the record-style definition, see
41 | ||| `Control.Category.Records.CartesianClosedR`.
42 | public export
43 | CartesianClosed : (cat : Hom obj) -> (ten,hom : obj -> obj -> obj) -> (i : obj) -> Type
44 | CartesianClosed cat ten hom i = (Cartesian cat ten i, Closed cat ten hom i)
45 |
46 |
47 | ------------------------------------------------------------
48 | -- Functions
49 | ------------------------------------------------------------
50 |
51 | ||| The evaluation map of a closed monoidal category.
52 | public export
53 | eval : Closed cat ten hom i => {a,b : _} -> cat ((a `hom` b) `ten` a) b
54 | eval @{c@(MkClosed{})} = uncurry id
55 |
56 | ||| The coevaluation map of a closed monoidal category.
57 | public export
58 | coeval : Closed cat ten hom i => {a,b : _} -> cat a (b `hom` (a `ten` b))
59 | coeval @{c@(MkClosed{})} = curry {ten} id
60 |
61 |
62 | ------------------------------------------------------------
63 | -- Existing Instances
64 | ------------------------------------------------------------
65 |
66 | public export
67 | Closed Morphism Pair Morphism () where
68 |   curry (Mor f) = Mor $ Mor . curry f
69 |   uncurry (Mor f) = Mor $ uncurry $ applyMor . f
70 |
71 | public export
72 | Closed Morphism Pair (~~>) () where
73 |   curry = Mor . curry . applyMor
74 |   uncurry = Mor . uncurry . applyMor
75 |
76 | namespace Closed
77 |   public export
78 |   [Function] Closed (~~>) Pair (~~>) ()
79 |       using Monoidal.FuncPair where
80 |     curry = Prelude.curry
81 |     uncurry = Prelude.uncurry
82 |