Control.Category.Instances.Zero

This module defines `Zero`, the zero category, which contains no
objects and no morphisms.

Definitions

data Zero : Void -> Void -> Type

  The zero category, or initial category. This category contains
  no objects and no morphisms.

Totality: total
Visibility: public export
Hints:

Bimonoidal Zero add mul z i

Braided Zero ten i

Cartesian Zero ten i

Either (catA = Zero) (Either (catB = Zero) (cat' = Zero)) => CatBifunctor catA catB cat' f

Either (cat = Zero) (cat' = Zero) => CatFunctor cat cat' f

CatMonad Zero m

Category Zero

Closed Zero ten hom i

Cocartesian Zero ten i

Monoidal Zero ten i

Semigroupoid Zero

Traced Zero ten i

Uninhabited (Zero a b)

Zero : SemigroupoidR

Totality: total
Visibility: public export

Zero : CategoryR

Totality: total
Visibility: public export

ZeroInitial : FunctorR Zero cat

Totality: total
Visibility: public export