This module defines the functor category between two categories, `FunCat C D`, traditionally written `[C, D]`. Its morphisms are natural transformations between parallel functors.
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.
FunProd : (ten : (cat' .obj -> cat' .obj -> cat' .obj)) -> CatEndoBifunctor (cat' .hom) ten => FunctorR cat cat' -> FunctorR cat cat' -> FunctorR cat cat'FunUnit : cat' .obj -> FunctorR cat cat'MonoidalFunCat : {auto {conArg:4703} : Monoidal (cat' .hom) ten i} -> Monoidal (FunCat cat cat') (FunProd ten) (FunUnit i)BraidedFunCat : {auto {conArg:5293} : Braided (cat' .hom) ten i} -> Braided (FunCat cat cat') (FunProd ten) (FunUnit i)CartesianFunCat : {auto {conArg:5590} : Cartesian (cat' .hom) ten i} -> Cartesian (FunCat cat cat') (FunProd ten) (FunUnit i)CocartesianFunCat : {auto {conArg:6088} : Cocartesian (cat' .hom) ten i} -> Cocartesian (FunCat cat cat') (FunProd ten) (FunUnit i)TracedFunCat : {auto {conArg:6586} : Traced (cat' .hom) ten i} -> Traced (FunCat cat cat') (FunProd ten) (FunUnit i)FunCat : CategoryR -> CategoryR -> CategoryRFunCat : CategoryR -> MonoidalR -> MonoidalRFunCat : CategoryR -> BraidedR -> BraidedRFunCat : CategoryR -> CartesianR -> CartesianRFunCat : CategoryR -> CocartesianR -> CocartesianRFunCat : CategoryR -> TracedR -> TracedR