
  0 | module Control.Category.Records.Semigroupoid
  1 | 
  2 | import Control.Category
  3 | 
  4 | %default total
  5 | %prefix_record_projections off
  6 | 
  7 | ||| A *semigroupoid* is a category that lacks identity morphisms.
  8 | |||
  9 | ||| Laws:
 10 | ||| * `(f . g) . h = f . (g . h)`
 11 | public export
 12 | record SemigroupoidR where
 13 |   constructor MkSemigroupoidR
 14 |   hom : Hom obj
 15 |   {auto impl : Semigroupoid hom}
 16 | 
 17 | namespace SemigroupoidR
 18 |   ||| Convert this into a `SemigroupoidR`.
 19 |   public export %inline
 20 |   (.semigroupoidR) : (rec : SemigroupoidR) -> SemigroupoidR
 21 |   (.semigroupoidR) = id
 22 | 
 23 |   ||| Binary right-to-left composition of morphisms.
 24 |   public export %inline
 25 |   (.comp) : (rec : SemigroupoidR) -> {a,b,c : _} ->
 26 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 27 |   (.comp) rec = (.) @{rec.impl}
 28 |