Control.Category.Instances.One

This module defines `Zero`, the one category, which contains one
single object and one identity morphism.

Definitions

data One : () -> () -> Type

  The one category, or terminal category. This category contains one
  object and one identity morphism.

Totality: total
Visibility: public export
Constructor: 

MkOne : One () ()

Hints:

Bimonoidal One UnitOp2 UnitOp2 () ()

Braided One UnitOp2 ()

Cartesian One UnitOp2 ()

CatBifunctor catA catB One UnitOp2

CatFunctor cat One UnitOp

CatMonad One UnitOp

Category One

Closed One UnitOp2 UnitOp2 ()

Cocartesian One UnitOp2 ()

MonSymmetric One UnitOp2 ()

Monoidal One UnitOp2 ()

Semigroupoid One

Traced One UnitOp2 ()

mkOne : One a b

Totality: total
Visibility: public export

UnitOp : a -> ()

Totality: total
Visibility: public export

UnitOp2 : a -> b -> ()

Totality: total
Visibility: public export

One : SemigroupoidR

Totality: total
Visibility: public export

One : CategoryR

Totality: total
Visibility: public export

One : MonoidalR

Totality: total
Visibility: public export

One : BraidedR

Totality: total
Visibility: public export

One : SymmetricR

Totality: total
Visibility: public export

One : CartesianR

Totality: total
Visibility: public export

One : CocartesianR

Totality: total
Visibility: public export

One : ClosedR

Totality: total
Visibility: public export

One : TracedR

Totality: total
Visibility: public export

One : BimonoidalR

Totality: total
Visibility: public export

One : RigCategoryR

Totality: total
Visibility: public export

One : SymRigCategoryR

Totality: total
Visibility: public export

One : DistributiveR

Totality: total
Visibility: public export

OneTerminal : FunctorR cat One

Totality: total
Visibility: public export

OneM : MonadR One

Totality: total
Visibility: public export

OneBi : BifunctorR catA catB One

Totality: total
Visibility: public export