Control.Category.Instances.Linear

(source)

This module defines `Linear`, the category of types and linear
functions. Unlike the unrestricted function category `Typ`, this
is a non-distributive bimonoidal category.

Reexports

import public Data.Linear

Definitions

data Linear : Type0 -> Type0 -> Type

  The category of types and linear functions.

Totality: total
Visibility: public export
Constructor:

MkLinear : (1 _ : a .runW0 -@ b .runW0) -> Linear a b

Hints:

Bimonoidal Linear LEither LPair (W0 Void) (W0 ())
Braided Linear LPair (W0 ())
Braided Linear LEither (W0 Void)
CatBifunctor Linear Linear Linear LPair
CatBifunctor Linear Linear Linear LEither
CatFunctor Linear Typ id
CatFunctor Linear Linear (liftW LMaybe)
Category Linear
Closed Linear LPair LinearHom (W0 ())
Monoidal Linear LPair (W0 ())
Monoidal Linear LEither (W0 Void)
Semigroupoid Linear

runLinear : Linear a b -@ (a .runW0 -@ b .runW0)

Totality: total
Visibility: public export

.runLinear : Linear a b -@ (a .runW0 -@ b .runW0)

Totality: total
Visibility: public export

Linear_ : (0 _ : Type) -> (0 _ : Type) -> Type

Totality: total
Visibility: public export

LPair : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

LEither : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

LinearHom : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

leither : a -@ c -> b -@ c -> LEither a b -@ c

Totality: total
Visibility: public export

LinearSemigroupoid : Semigroupoid Linear

Totality: total
Visibility: public export

Linear : SemigroupoidR

Totality: total
Visibility: public export

Linear : CategoryR

Totality: total
Visibility: public export

LinearToTyp : FunctorR Linear Typ

Totality: total
Visibility: public export

LMaybe : EndofunctorR Linear

Totality: total
Visibility: public export

LPair : EndoBifunctorR Linear

Totality: total
Visibility: public export

LEither : EndoBifunctorR Linear

Totality: total
Visibility: public export

LinearLPair : MonoidalR

Totality: total
Visibility: public export

LinearLEither : MonoidalR

Totality: total
Visibility: public export

LinearLPair : BraidedR

Totality: total
Visibility: public export

LinearLEither : BraidedR

Totality: total
Visibility: public export

Linear : BimonoidalR

Totality: total
Visibility: public export

Linear : RigCategoryR

Totality: total
Visibility: public export

Linear : SymRigCategoryR

Totality: total
Visibility: public export

Linear : ClosedR

Totality: total
Visibility: public export