Control.Category.Instances.Cat

(source)

This module defines the category of categories, `Cat`, whose
morphisms are functors.

Definitions

Cat : Hom CategoryR

  The category of categories.

Totality: total
Visibility: public export

record Cat0 : Wrap0 CategoryR -> Wrap0 CategoryR -> Type

  The erased category of categories.
  
  This category is identical to `Cat`, except its category objects
  are not required to exist at runtime. This makes it more efficient
  at the cost of restricting its capabilities.

Totality: total
Visibility: public export
Constructor:

MkCat0 : Cat (a .runW0) (b .runW0) -> Cat0 a b

Projection:

.runCat0 : Cat0 a b -> Cat (a .runW0) (b .runW0)

Hints:

Bimonoidal Cat0 Cat0Sum Cat0Prod (W0 Zero) (W0 One)
Braided Cat0 Cat0Prod (W0 One)
Braided Cat0 Cat0Sum (W0 Zero)
Cartesian Cat0 Cat0Prod (W0 One)
CatBifunctor Cat0 Cat0 Cat0 Cat0Prod
CatBifunctor Cat0 Cat0 Cat0 Cat0Sum
Category Cat0
Cocartesian Cat0 Cat0Sum (W0 Zero)
MonSymmetric Cat0 Cat0Prod (W0 One)
MonSymmetric Cat0 Cat0Sum (W0 Zero)
Monoidal Cat0 Cat0Prod (W0 One)
Monoidal Cat0 Cat0Sum (W0 Zero)
Semigroupoid Cat0

.runCat0 : Cat0 a b -> Cat (a .runW0) (b .runW0)

Totality: total
Visibility: public export

runCat0 : Cat0 a b -> Cat (a .runW0) (b .runW0)

Totality: total
Visibility: public export

Cat0_ : Hom CategoryR

Totality: total
Visibility: public export

Cat0Prod : Wrap0 CategoryR -> Wrap0 CategoryR -> Wrap0 CategoryR

Totality: total
Visibility: public export

Cat0Sum : Wrap0 CategoryR -> Wrap0 CategoryR -> Wrap0 CategoryR

Totality: total
Visibility: public export

SemigroupoidCat : Semigroupoid Cat

Totality: total
Visibility: public export

SymmetricCatProd : MonSymmetric Cat Prod One

Totality: total
Visibility: public export

SymmetricCatSum : MonSymmetric Cat Sum Zero

Totality: total
Visibility: public export

SemigroupoidCat0 : Semigroupoid Cat0

Totality: total
Visibility: public export

SymmetricCat0Prod : MonSymmetric Cat0 Cat0Prod (W0 One)

Totality: total
Visibility: public export

SymmetricCat0Sum : MonSymmetric Cat0 Cat0Sum (W0 Zero)

Totality: total
Visibility: public export

Cat : SemigroupoidR

Totality: total
Visibility: public export

Cat0 : SemigroupoidR

Totality: total
Visibility: public export

Cat : CategoryR

Totality: total
Visibility: public export

Cat0 : CategoryR

Totality: total
Visibility: public export

CatProd : MonoidalR

Totality: total
Visibility: public export

CatSum : MonoidalR

Totality: total
Visibility: public export

Cat0Prod : MonoidalR

Totality: total
Visibility: public export

Cat0Sum : MonoidalR

Totality: total
Visibility: public export

CatProd : BraidedR

Totality: total
Visibility: public export

CatSum : BraidedR

Totality: total
Visibility: public export

Cat0Prod : BraidedR

Totality: total
Visibility: public export

Cat0Sum : BraidedR

Totality: total
Visibility: public export

CatProd : SymmetricR

Totality: total
Visibility: public export

CatSum : SymmetricR

Totality: total
Visibility: public export

Cat0Prod : SymmetricR

Totality: total
Visibility: public export

Cat0Sum : SymmetricR

Totality: total
Visibility: public export

Cat : CartesianR

Totality: total
Visibility: public export

Cat0 : CartesianR

Totality: total
Visibility: public export

Cat : CocartesianR

Totality: total
Visibility: public export

Cat0 : CocartesianR

Totality: total
Visibility: public export

Cat : BimonoidalR

Totality: total
Visibility: public export

Cat0 : BimonoidalR

Totality: total
Visibility: public export

Cat : RigCategoryR

Totality: total
Visibility: public export

Cat0 : RigCategoryR

Totality: total
Visibility: public export

Cat : SymRigCategoryR

Totality: total
Visibility: public export

Cat0 : SymRigCategoryR

Totality: total
Visibility: public export

Cat : DistributiveR

Totality: total
Visibility: public export

Cat0 : DistributiveR

Totality: total
Visibility: public export

Cat : ClosedR

Totality: total
Visibility: public export

Cat : CartesianClosedR

Totality: total
Visibility: public export