
  0 | module Control.Category.Records.Category
  1 | 
  2 | import Control.Category
  3 | import Control.Category.Records.Semigroupoid
  4 | 
  5 | %default total
  6 | %prefix_record_projections off
  7 | 
  8 | ||| A *category* is a generalized function type with a notion of
  9 | ||| composition and of identity. The elements of this type are
 10 | ||| typically called *morphisms*.
 11 | |||
 12 | ||| See `Category` for required laws.
 13 | public export
 14 | record CategoryR where
 15 |   constructor MkCategoryR
 16 |   hom : Hom obj
 17 |   {auto impl : Category hom}
 18 | 
 19 | namespace CategoryR
 20 |   ||| Convert this into a `SemigroupoidR`.
 21 |   public export %inline
 22 |   (.semigroupoidR) : (rec : CategoryR) -> SemigroupoidR
 23 |   (.semigroupoidR) (MkCategoryR {} {hom}) = MkSemigroupoidR hom {impl = FromCategory}
 24 | 
 25 | 
 26 |   ||| Convert this into a `CategoryR`.
 27 |   public export %inline
 28 |   (.categoryR) : (rec : CategoryR) -> CategoryR
 29 |   (.categoryR) = id
 30 | 
 31 |   ||| The identity morphism of an object `a`.
 32 |   public export %inline
 33 |   (.id) : (rec : CategoryR) -> {a : _} -> rec.hom a a
 34 |   (.id) rec = id @{rec.impl}
 35 | 
 36 |   ||| Binary right-to-left composition of morphisms.
 37 |   public export %inline
 38 |   (.comp) : (rec : CategoryR) -> {a,b,c : _} ->
 39 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 40 |   (.comp) rec = (.) @{rec.impl}
 41 |