record SemigroupoidR : Type A *semigroupoid* is a category that lacks identity morphisms.
Laws:
* `(f . g) . h = f . (g . h)`
Totality: total
Visibility: public export
Constructor: MkSemigroupoidR : (hom : Hom obj) -> Semigroupoid hom => SemigroupoidR
Projections:
.comp : (rec : SemigroupoidR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.hom : ({rec:0} : SemigroupoidR) -> Hom ({rec:0} .obj).impl : ({rec:0} : SemigroupoidR) -> Semigroupoid ({rec:0} .hom)0 .obj : SemigroupoidR -> Type.semigroupoidR : SemigroupoidR -> SemigroupoidR Convert this into a `SemigroupoidR`.
.hom : ({rec:0} : SemigroupoidR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .impl : ({rec:0} : SemigroupoidR) -> Semigroupoid ({rec:0} .hom)- Totality: total
Visibility: public export .semigroupoidR : SemigroupoidR -> SemigroupoidR Convert this into a `SemigroupoidR`.
Totality: total
Visibility: public export.comp : (rec : SemigroupoidR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export