Control.Category.Instances.FunCat

(source)

This module defines the functor category between two categories,
`FunCat C D`, traditionally written `[C, D]`. Its morphisms are
natural transformations between parallel functors.

Definitions

FunCat : (cat : CategoryR) -> (cat' : CategoryR) -> Hom (FunctorR cat cat')

  The functor category between `cat` and `cat'`.
  
  This category doesn't play very nicely with Idris's interface
  resolution. Consider using the record-style definitions below.

Totality: total
Visibility: public export

FunProd : (ten : (cat' .obj -> cat' .obj -> cat' .obj)) -> CatEndoBifunctor (cat' .hom) ten => FunctorR cat cat' -> FunctorR cat cat' -> FunctorR cat cat'

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

MonoidalFunCat : {auto {conArg:4712} : Monoidal (cat' .hom) ten i} -> Monoidal (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

BraidedFunCat : {auto {conArg:5302} : Braided (cat' .hom) ten i} -> Braided (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

SymmetricFunCat : {auto {conArg:5599} : MonSymmetric (cat' .hom) ten i} -> MonSymmetric (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

CartesianFunCat : {auto {conArg:5731} : Cartesian (cat' .hom) ten i} -> Cartesian (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

CocartesianFunCat : {auto {conArg:6229} : Cocartesian (cat' .hom) ten i} -> Cocartesian (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

TracedFunCat : {auto {conArg:6727} : Traced (cat' .hom) ten i} -> Traced (FunCat cat cat') (FunProd ten) (FunUnit i)

Totality: total
Visibility: public export

FunCat : CategoryR -> CategoryR -> CategoryR

Totality: total
Visibility: public export

FunCat : CategoryR -> MonoidalR -> MonoidalR

Totality: total
Visibility: public export

FunCat : CategoryR -> BraidedR -> BraidedR

Totality: total
Visibility: public export

FunCat : CategoryR -> SymmetricR -> SymmetricR

Totality: total
Visibility: public export

FunCat : CategoryR -> CartesianR -> CartesianR

Totality: total
Visibility: public export

FunCat : CategoryR -> CocartesianR -> CocartesianR

Totality: total
Visibility: public export

FunCat : CategoryR -> TracedR -> TracedR

Totality: total
Visibility: public export