0 | module Data.Container
 1 |
 2 | import public Data.Product
 3 | import public Data.Coproduct
 4 | import public Data.Sigma
 5 | import public Data.Category.Ops
 6 |
 7 | import Proofs.Congruence
 8 | import Proofs.Extensionality
 9 |
10 | %default total
11 |
12 | ||| A container is a product of a type for requestsions and a type of responses indexed by the requests
13 | ||| They can be used to describe data types
14 | public export
15 | record Container where
16 |   constructor (!>)
17 |   ||| Requests/Queries/Inputs
18 |   req : Type
19 |   ||| Responses/Results/Outputs
20 |   res : req -> Type
21 |
22 | %pair Container req res
23 |
24 | ||| A constructor for containers where the responses do not depend on the requests
25 | public export
26 | (:-) : Type -> Type -> Container
27 | (:-) x y = (!>) x (const y)
28 |
29 | ||| The unit for containers
30 | public export
31 | CUnit : Container
32 | CUnit = Unit :- Unit
33 |
34 | ||| The neutral for composition
35 | public export
36 | CNeutral : Container
37 | CNeutral = Unit :- Void
38 |
39 | ||| The coproduct on containers, neutral is CVoid
40 | public export
41 | (+) : (c1, c2 : Container) -> Container
42 | (+) c1 c2 = (!>) (c1.req + c2.req) (choice c1.res c2.res)
43 |
44 | ||| The tensor on containers, neutral element is CUnit
45 | public export
46 | (⊗) : (c1, c2 : Container) -> Container
47 | (⊗) c1 c2 = (x : c1.req * c2.req) !> c1.res x.π1 * c2.res x.π2
48 |
49 | ||| Extension of a container as a functor
50 | public export
51 | record Ex (cont : Container) (ty : Type) where
52 |   constructor MkEx
53 |   ex1 : cont.req
54 |   ex2 : cont.res ex1 -> ty
55 |
56 | %pair Ex ex1 ex2
57 |
58 | public export
59 | record ExEq {a : Container} {b : Type} (c1, c2 : Ex a b) where
60 |   constructor MkExEq
61 |   pex1 : c1.ex1 === c2.ex1
62 |   pex2 : (v : a.res c1.ex1) ->
63 |          let 0 b1, b2 : b
64 |              b1 = c1.ex2 v
65 |              b2 = c2.ex2 (rewrite__impl a.res (sym pex1) v)
66 |           in b1 === b2
67 |
68 | public export
69 | 0 exEqToEq : ExEq c1 c2 -> c1 === c2
70 | exEqToEq {c1 = MkEx x1 x2} {c2 = MkEx y1 y2} (MkExEq x y) =
71 |   cong2Dep MkEx x (funExt $ y)
72 |