Control.Category.Records.Traced

Definitions

record TracedR : 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.
  
  See `Traced` for required laws.

Totality: total
Visibility: public export
Constructor:

MkTracedR : (hom : Hom obj) -> (tensor : (obj -> obj -> obj)) -> (unit : obj) -> Traced hom tensor unit => TracedR

Projections:

.assoc : (rec : TracedR) -> rec .hom (rec .tensor (rec .tensor a b) c) (rec .tensor a (rec .tensor b c))

  The left-biased associator. This must be the inverse of `(.assoc')`.

.assoc' : (rec : TracedR) -> rec .hom (rec .tensor a (rec .tensor b c)) (rec .tensor (rec .tensor a b) c)

  The right-biased associator. This must be the inverse of `(.assoc)`.

.categoryR : TracedR -> CategoryR

  Convert this into a `CategoryR`.

.comp : (rec : TracedR) -> rec .hom b c -> rec .hom a b -> rec .hom a c

  Binary right-to-left composition of morphisms.

.hom : ({rec:0} : TracedR) -> Hom ({rec:0} .obj)

.id : (rec : TracedR) -> rec .hom a a

  The identity morphism of an object `a`.

.impl : ({rec:0} : TracedR) -> Traced ({rec:0} .hom) ({rec:0} .tensor) ({rec:0} .unit)

.monoidalR : TracedR -> MonoidalR

  Convert this into a `MonoidalR`.

0 .obj : TracedR -> Type

.tensor : ({rec:0} : TracedR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj

.tensorR : (rec : TracedR) -> EndoBifunctorR (rec .categoryR)

  Return the tensor product as a `BifunctorR`.

.trace : (rec : TracedR) -> rec .hom a a -> rec .hom (rec .unit) (rec .unit)

  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) ]`.

.tracedR : TracedR -> TracedR

  Convert this into a `TracedR`.

.tracel : (rec : TracedR) -> rec .hom (rec .tensor a b) (rec .tensor a c) -> rec .hom b c

  The left trace.

.tracer : (rec : TracedR) -> rec .hom (rec .tensor a c) (rec .tensor b c) -> rec .hom a b

  The right trace.

.unit : ({rec:0} : TracedR) -> {rec:0} .obj

.unitl : (rec : TracedR) -> rec .hom (rec .tensor (rec .unit) a) a

  The left unitor.

.unitl' : (rec : TracedR) -> rec .hom a (rec .tensor (rec .unit) a)

  The inverse of `(.unitl)`, the left unitor.

.unitr : (rec : TracedR) -> rec .hom (rec .tensor a (rec .unit)) a

  The right unitor.

.unitr' : (rec : TracedR) -> rec .hom a (rec .tensor a (rec .unit))

  The inverse of `(.unitr)`, the right unitor.

.hom : ({rec:0} : TracedR) -> Hom ({rec:0} .obj)