0 | module Data.Category.Graded
 1 |
 2 | import public Data.List.Quantifiers as QL
 3 |
 4 | -- free monoid using the coproduct on types
 5 | public export
 6 | OneOf : List Type -> Type
 7 | OneOf = QL.Any.Any id
 8 |
 9 | -- Left and right injection for OneOf
10 | namespace Any
11 |   export
12 |   left : QL.Any.Any p xs -> QL.Any.Any p (xs ++ ys)
13 |   left (Here x) = Here x
14 |   left (There x) = There (left x)
15 |
16 |   export
17 |   right : {ys : _} -> QL.Any.Any p xs -> QL.Any.Any p (ys ++ xs)
18 |   right {ys = []} x = x
19 |   right {ys = (y :: ys)} x = There (right x)
20 |
21 |
22 |
23 | -- A Graded category is one where the morphisms are indexed by a monoid `gr` representing the grade.
24 | public export
25 | interface GradedCat (mon : Monoid gr) (0 arr : gr -> obj -> obj -> Type) | arr where
26 |   constructor MkGradedCat
27 |
28 |   -- the identity morphism has the neutral element of the monoid as grade
29 |   identity : forall x. arr Prelude.Interfaces.neutral x x
30 |
31 |   -- The composition combines each grade from both morphisms using the monoidal product
32 |   (#>) : forall x, y, z.  {g1, g2 : _} -> arr g1 x y -> arr g2 y z -> arr (g1 <+> g2) x z
33 |
34 | export infixr 1 #>
35 |
36 | -- The coproduct semigroup on types
37 | public export
38 | [EitherSem] Semigroup Type where
39 |   (<+>) = Either
40 |
41 | -- The coproduct monoid on types
42 | public export
43 | [EitherMon] Monoid Type using EitherSem where
44 |   neutral = Void
45 |
46 | -- The free semigroup on types
47 | public export
48 | [AnySem] Semigroup (List Type) where
49 |   (<+>) = (++)
50 |
51 | -- The free monoid on types
52 | public export
53 | [AnyMon] Monoid (List Type) using EitherSem where
54 |   neutral = []
55 |
56 | -- A graded coproduct monad is a morphism in Set where the codomain
57 | -- is `Either` the morphism is graded by the `Left` type of the `Either`
58 | -- The left side is not the grade itself but the result of applying the functor `f : gr -> Type`
59 | -- This way the grade and the morphism can be different
60 | public export
61 | GradedCoproductMonad : {0 e : Type} -> (e -> Type) -> e -> Type -> Type -> Type
62 | GradedCoproductMonad  f e x y = (x -> Either (f e) y)
63 |
64 | -- We can define graded coproduct morphisms with the `Either` type as the grade
65 | public export
66 | EitherGradeMor : Type -> Type -> Type -> Type
67 | EitherGradeMor e x y = GradedCoproductMonad id e x y
68 |
69 | -- We can define graded coproduct morphisms with `List Type` as the grade and `OneOf` as the functor to interpret the grade
70 | public export
71 | AnyErrGradeMor : List Type -> Type -> Type -> Type
72 | AnyErrGradeMor e x y = GradedCoproductMonad OneOf e x y
73 |
74 |