
  0 | module Data.Container.Morphism
  1 | 
  2 | import public Data.Container
  3 | 
  4 | import Control.Order
  5 | import Control.Relation
  6 | 
  7 | ||| A container morphism
  8 | public export
  9 | record (=%>) (c1, c2 : Container) where
 10 |   constructor (<|)
 11 |   fwd : c1.req -> c2.req
 12 |   bwd : (x : c1.req) -> c2.res (fwd x) -> c1.res x
 13 | 
 14 | %pair (=%>) fwd bwd
 15 | 
 16 | ||| Identity of container morphisms
 17 | public export
 18 | identity : a =%> a
 19 | identity = id <| (\_ => id)
 20 | 
 21 | public export
 22 | (⨾) : a =%> b -> b =%> c -> a =%> c
 23 | (⨾) x y = (y.fwd . x.fwd) <| (\z => x.bwd z . y.bwd (x.fwd z))
 24 | 
 25 | public export
 26 | embed : {0 a : Type} -> {0 b : a -> Type} -> (f : (x : a) -> b x) ->
 27 |     ((!>) a b) =%> CUnit
 28 | embed f = (\_ => ()) <| (\x, _ => f x)
 29 | 
 30 | public export
 31 | extract : ((!>) a b) =%> CUnit -> (x : a) -> b x
 32 | extract c x = c.bwd x ()
 33 | 
 34 | public export
 35 | unit : CUnit ⊗ CUnit =%> CUnit
 36 | unit =
 37 |   (\_ => ()) <|
 38 |   (\_, _ => () && ())
 39 | 
 40 | public export
 41 | dia : a + a =%> a
 42 | dia =
 43 |   dia <|
 44 |   (\case (+> r) => id
 45 |          (<+ l) => id)
 46 | 
 47 | public export
 48 | Reflexive Container (=%>) where
 49 |   reflexive = identity
 50 | 
 51 | public export
 52 | Transitive Container (=%>) where
 53 |   transitive = (⨾)
 54 | 
 55 | public export
 56 | Preorder Container (=%>) where
 57 |