
  0 | module Data.Category
  1 | 
  2 | import public Data.Category.Ops
  3 | 
  4 | private infixr 1 ~:>  -- Explicit morphism
  5 | private infixl 5 |:>  -- Explicit composition
  6 | 
  7 | public export
  8 | record Category (o : Type) where
  9 |   constructor MkCategory
 10 |   0 (~:>) : o -> o -> Type
 11 |   id : (v : o) -> v ~:> v
 12 |   (|:>) : {0 a, b, c : o} -> (a ~:> b) -> (b ~:> c) -> (a ~:> c)
 13 |   0 idLeft : {a, b : o} -> (f : a ~:> b) -> f |:> id b = f
 14 |   0 idRight : {a, b : o} -> (f : a ~:> b) -> id a |:> f = f
 15 |   0 compAssoc : {a, b, c, d : o} ->
 16 |                 (f : a ~:> b) ->
 17 |                 (g : b ~:> c) ->
 18 |                 (h : c ~:> d) ->
 19 |                 f |:> (g |:> h) = (f |:> g) |:> h
 20 | 
 21 | -- An operator for morphisms without passing the category in argument
 22 | public export
 23 | 0 (~>) : (cat : Category o) => o -> o -> Type
 24 | (~>) = Category.(~:>) cat
 25 | 
 26 | -- An operator for sequential composition without passing in the category in argument
 27 | public export
 28 | (|>) : (cat : Category o) => {0 a, b, c : o} ->
 29 |        a ~> b -> b ~> c -> a ~> c
 30 | (|>) = Category.(|:>) cat
 31 | 
 32 | -- The opposite category
 33 | public export
 34 | (.op) : Category o -> Category o
 35 | (.op) cat = MkCategory
 36 |     (\x, y => y ~> x)
 37 |     (cat.id)
 38 |     (\f, g => (|:>) cat g f )
 39 |     (cat.idRight)
 40 |     (cat.idLeft)
 41 |     (\f, g, h => sym (cat.compAssoc h g f))
 42 | 
 43 | public export
 44 | Idris : Category Type
 45 | Idris = MkCategory
 46 |   (\a, b => a -> b)
 47 |   (\_ => id)
 48 |   (\f, g => g . f)
 49 |   (\_ => Refl)
 50 |   (\_ => Refl)
 51 |   (\_, _, _ => Refl)
 52 |