Control.Category.Traced

Definitions

interface Traced : Hom obj -> (obj -> obj -> obj) -> obj -> Type

  A *traced monoidal category* is a monoidal category equipped with
  trace maps, maps which allow one to write loops in string diagrams.
  The name "traced" comes from a connection to the trace of a matrix
  in linear algebra, though the concept has far greater applications.
  
  This is the interface-style definition of a traced monoidal category.
  For the record-style definition, see `Control.Category.Records.TracedR`.
  
  Laws:
  * `tracel (mapr f . g) = f . tracel g`
  * `tracer (mapl f . g) = f . tracer g`
  * `tracel (f . mapr g) = tracel f . g`
  * `tracer (f . mapl g) = tracer f . g`
  * `tracel (unitl' . f . unitl) = f`
  * `tracer (unitr' . f . unitr) = f`
  * `tracel (tracel f) . assoc = tracel f`
  * `tracer (tracer f) . assoc' = tracer f`
  * `assoc . tracer (bimap f g) = bimap f (tracer g)`
  * `assoc' . tracel (bimap f g) = bimap (tracel f) g`
  * `tracel f = tracer f` for all `f : cat a a`
  
  Note that these laws are for spherical traces, which are rather
  restrictive. Some weaker versions of these laws may be appropriate
  depending on the needs of the implementation.

Parameters: cat, ten, i
Constraints: Monoidal cat ten i
Constructor: 

MkTraced

Methods:

tracel : cat (ten a b) (ten a c) -> cat b c

  The left trace.

tracer : cat (ten a c) (ten b c) -> cat a b

  The right trace.

tracel : Traced cat ten i => cat (ten a b) (ten a c) -> cat b c

  The left trace.

Totality: total
Visibility: public export

tracer : Traced cat ten i => cat (ten a c) (ten b c) -> cat a b

  The right trace.

Totality: total
Visibility: public export

PreTraced : Hom obj -> (obj -> obj -> obj) -> obj -> Type

  See `PreMonoidal`.

Totality: total
Visibility: public export

trace : Traced cat ten i => cat a a -> cat i i

  Take the trace of an endomorphism, returning an endomorphism in
  the unit object. Depending on what the unit object is, this may
  or may not actually be useful.
  
  The name comes from the fact that in the monoidal category of
  vector spaces, this takes a square matrix `M` to the 1x1 matrix
  `[ tr(M) ]`.

Totality: total
Visibility: public export