Control.Category.Records.Functor

Definitions

record FunctorR : CategoryR -> CategoryR -> Type

  A *functor* is a mapping between categories that preserves their
  structure.
  
  See `CatFunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkFunctorR : (fun : (cat .obj -> cat' .obj)) -> CatFunctor (cat .hom) (cat' .hom) fun => FunctorR cat cat'

Projections:

.fun : FunctorR cat cat' -> cat .obj -> cat' .obj

.functorR : FunctorR cat cat' -> FunctorR cat cat'

  Convert this into a `FunctorR`.

.impl : ({rec:0} : FunctorR cat cat') -> CatFunctor (cat .hom) (cat' .hom) ({rec:0} .fun)

.map : (rec : FunctorR cat cat') -> cat .hom a b -> cat' .hom (rec .fun a) (rec .fun b)

  Apply the functor to a morphism in `cat`, translating it into `cat'`.

.fun : FunctorR cat cat' -> cat .obj -> cat' .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : FunctorR cat cat') -> CatFunctor (cat .hom) (cat' .hom) ({rec:0} .fun)

Totality: total
Visibility: public export

EndofunctorR : CategoryR -> Type

  A type synonym for an *endofunctor*, a functor from a category to
  itself.

Totality: total
Visibility: public export

.functorR : FunctorR cat cat' -> FunctorR cat cat'

  Convert this into a `FunctorR`.

Totality: total
Visibility: public export

.map : (rec : FunctorR cat cat') -> cat .hom a b -> cat' .hom (rec .fun a) (rec .fun b)

  Apply the functor to a morphism in `cat`, translating it into `cat'`.

Totality: total
Visibility: public export

record BifunctorR : CategoryR -> CategoryR -> CategoryR -> Type

  A *bifunctor* is a binary functor, i.e. a functor that maps two
  categories to one.
  
  See `CatBifunctor` for required laws.

Totality: total
Visibility: public export
Constructor: 

MkBifunctorR : (fun : (catA .obj -> catB .obj -> cat' .obj)) -> CatBifunctor (catA .hom) (catB .hom) (cat' .hom) fun => BifunctorR catA catB cat'

Projections:

.bimap : (rec : BifunctorR catA catB cat') -> catA .hom a b -> catB .hom a' b' -> cat' .hom (rec .fun a a') (rec .fun b b')

  Apply the bifunctor to morphism in `catA` and `catB`, translating
  them into a combined morphism in `cat'`.

.fun : BifunctorR catA catB cat' -> catA .obj -> catB .obj -> cat' .obj

.impl : ({rec:0} : BifunctorR catA catB cat') -> CatBifunctor (catA .hom) (catB .hom) (cat' .hom) ({rec:0} .fun)

.left : BifunctorR catA catB cat' -> catB .obj -> FunctorR catA cat'

  Convert a bifunctor (or binoidal functor) into its left functor.

.mapl : (rec : BifunctorR catA catB cat') -> catA .hom a b -> cat' .hom (rec .fun a c) (rec .fun b c)

  Apply a morphism to a bifunctor only on the left.

.mapr : (rec : BifunctorR catA catB cat') -> catB .hom a b -> cat' .hom (rec .fun c a) (rec .fun c b)

  Apply a morphism to a bifunctor only on the right.

.right : BifunctorR catA catB cat' -> catA .obj -> FunctorR catB cat'

  Convert a bifunctor (or binoidal functor) into its right functor.

.fun : BifunctorR catA catB cat' -> catA .obj -> catB .obj -> cat' .obj

Totality: total
Visibility: public export

.impl : ({rec:0} : BifunctorR catA catB cat') -> CatBifunctor (catA .hom) (catB .hom) (cat' .hom) ({rec:0} .fun)

Totality: total
Visibility: public export

BinoidalR : CategoryR -> CategoryR -> CategoryR -> Type

  See `Binoidal`.

Totality: total
Visibility: public export

EndoBifunctorR : CategoryR -> Type

  A type synonym for an *endo-bifunctor*, a bifunctor from a category
  to itself.

Totality: total
Visibility: public export

EndoBinoidalR : CategoryR -> Type

  See `Binoidal`.

Totality: total
Visibility: public export

.bimap : (rec : BifunctorR catA catB cat') -> catA .hom a b -> catB .hom a' b' -> cat' .hom (rec .fun a a') (rec .fun b b')

  Apply the bifunctor to morphism in `catA` and `catB`, translating
  them into a combined morphism in `cat'`.

Totality: total
Visibility: public export

.mapl : (rec : BifunctorR catA catB cat') -> catA .hom a b -> cat' .hom (rec .fun a c) (rec .fun b c)

  Apply a morphism to a bifunctor only on the left.

Totality: total
Visibility: public export

.mapr : (rec : BifunctorR catA catB cat') -> catB .hom a b -> cat' .hom (rec .fun c a) (rec .fun c b)

  Apply a morphism to a bifunctor only on the right.

Totality: total
Visibility: public export

.left : BifunctorR catA catB cat' -> catB .obj -> FunctorR catA cat'

  Convert a bifunctor (or binoidal functor) into its left functor.

Totality: total
Visibility: public export

.right : BifunctorR catA catB cat' -> catA .obj -> FunctorR catB cat'

  Convert a bifunctor (or binoidal functor) into its right functor.

Totality: total
Visibility: public export