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)
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

SemigroupoidCat0 : Semigroupoid Cat0

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

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