gdritter repos pico-ml-old / master stdlib / Category.pml
master

Tree @master (Download .tar.gz)

Category.pml @masterraw · history · blame

exports
  Category(..)
  _>>>_
  _<<<_
  arrowCategory

record Category cat
  .id      (cat a a)
  .compose (cat b c -> cat a b -> cat a c)

_>>>_ : implicit (Category cat) -> cat a b -> cat b c -> cat a c
  c = flip c.compose

_<<<_ : implicit (Category cat) -> cat b c -> cat a b -> cat a c
  c = c.compose

implicit arrowCategory : Category _->_ = rec
  .id      = id
  .compose = compose