record CategoryR : Type A *category* is a generalized function type with a notion of
composition and of identity. The elements of this type are
typically called *morphisms*.
See `Category` for required laws.
Totality: total
Visibility: public export
Constructor: MkCategoryR : (hom : Hom obj) -> Category hom => CategoryR
Projections:
.categoryR : CategoryR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : CategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.hom : ({rec:0} : CategoryR) -> Hom ({rec:0} .obj).id : (rec : CategoryR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : CategoryR) -> Category ({rec:0} .hom)0 .obj : CategoryR -> Type.semigroupoidR : CategoryR -> SemigroupoidR Convert this into a `SemigroupoidR`.
.hom : ({rec:0} : CategoryR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .impl : ({rec:0} : CategoryR) -> Category ({rec:0} .hom)- Totality: total
Visibility: public export .semigroupoidR : CategoryR -> SemigroupoidR Convert this into a `SemigroupoidR`.
Totality: total
Visibility: public export.categoryR : CategoryR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : CategoryR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : CategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export