0 | module Control.Category.Records.Traced
  1 |
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Functor
  5 | import Control.Category.Records.Monoidal
  6 | import Data.Morphisms
  7 |
  8 | %default total
  9 | %prefix_record_projections off
 10 |
 11 | ||| A *traced monoidal category* is a monoidal category equipped with
 12 | ||| trace maps, maps which allow one to write loops in string diagrams.
 13 | ||| The name "traced" comes from a connection to the trace of a matrix
 14 | ||| in linear algebra, though the concept has far greater applications.
 15 | |||
 16 | ||| See `Traced` for required laws.
 17 | public export
 18 | record TracedR where
 19 |   constructor MkTracedR
 20 |   hom : Hom obj
 21 |   tensor : obj -> obj -> obj
 22 |   unit : obj
 23 |   {auto impl : Traced hom tensor unit}
 24 |
 25 | ||| See `PreMonoidal`.
 26 | public export
 27 | PreTracedR : Type
 28 | PreTracedR = TracedR
 29 |
 30 | namespace TracedR
 31 |   ||| Convert this into a `CategoryR`.
 32 |   public export %inline
 33 |   (.categoryR) : (rec : TracedR) -> CategoryR
 34 |   (.categoryR) (MkTracedR {} {hom}) = MkCategoryR hom
 35 |
 36 |   ||| The identity morphism of an object `a`.
 37 |   public export %inline
 38 |   (.id) : (rec : TracedR) -> {a : _} -> rec.hom a a
 39 |   (.id) rec@(MkTracedR {}) = rec.categoryR.id
 40 |
 41 |   ||| Binary right-to-left composition of morphisms.
 42 |   public export %inline
 43 |   (.comp) : (rec : TracedR) -> {a,b,c : _} ->
 44 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 45 |   (.comp) rec@(MkTracedR {}) = rec.categoryR.comp
 46 |
 47 |
 48 |   ||| Return the tensor product as a `BifunctorR`.
 49 |   public export %inline
 50 |   (.tensorR) : (rec : TracedR) -> EndoBifunctorR rec.categoryR
 51 |   (.tensorR) (MkTracedR {} {tensor}) = MkBifunctorR tensor
 52 |
 53 |
 54 |   ||| Convert this into a `MonoidalR`.
 55 |   public export %inline
 56 |   (.monoidalR) : (rec : TracedR) -> MonoidalR
 57 |   (.monoidalR) (MkTracedR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
 58 |
 59 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
 60 |   public export %inline
 61 |   (.assoc) : (rec : TracedR) -> {a,b,c : _} ->
 62 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
 63 |   (.assoc) rec@(MkTracedR {}) = rec.monoidalR.assoc
 64 |
 65 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
 66 |   public export %inline
 67 |   (.assoc') : (rec : TracedR) -> {a,b,c : _} ->
 68 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
 69 |   (.assoc') rec@(MkTracedR {}) = rec.monoidalR.assoc'
 70 |
 71 |   ||| The left unitor.
 72 |   public export %inline
 73 |   (.unitl) : (rec : TracedR) -> {a : _} ->
 74 |              rec.hom (rec.tensor rec.unit a) a
 75 |   (.unitl) rec@(MkTracedR {}) = rec.monoidalR.unitl
 76 |
 77 |   ||| The inverse of `(.unitl)`, the left unitor.
 78 |   public export %inline
 79 |   (.unitl') : (rec : TracedR) -> {a : _} ->
 80 |               rec.hom a (rec.tensor rec.unit a)
 81 |   (.unitl') rec@(MkTracedR {}) = rec.monoidalR.unitl'
 82 |
 83 |   ||| The right unitor.
 84 |   public export %inline
 85 |   (.unitr) : (rec : TracedR) -> {a : _} ->
 86 |              rec.hom (rec.tensor a rec.unit) a
 87 |   (.unitr) rec@(MkTracedR {}) = rec.monoidalR.unitr
 88 |
 89 |   ||| The inverse of `(.unitr)`, the right unitor.
 90 |   public export %inline
 91 |   (.unitr') : (rec : TracedR) -> {a : _} ->
 92 |               rec.hom a (rec.tensor a rec.unit)
 93 |   (.unitr') rec@(MkTracedR {}) = rec.monoidalR.unitr'
 94 |
 95 |
 96 |   ||| Convert this into a `TracedR`.
 97 |   public export %inline
 98 |   (.tracedR) : (rec : TracedR) -> TracedR
 99 |   (.tracedR) = id
100 |
101 |   ||| The left trace.
102 |   public export %inline
103 |   (.tracel) : (rec : TracedR) -> {a,b,c : _} ->
104 |               rec.hom (rec.tensor a b) (rec.tensor a c) -> rec.hom b c
105 |   (.tracel) rec = tracel @{rec.impl}
106 |
107 |   ||| The right trace.
108 |   public export %inline
109 |   (.tracer) : (rec : TracedR) -> {a,b,c : _} ->
110 |               rec.hom (rec.tensor a c) (rec.tensor b c) -> rec.hom a b
111 |   (.tracer) rec = tracer @{rec.impl}
112 |
113 |   ||| Take the trace of an endomorphism, returning an endomorphism in
114 |   ||| the unit object. Depending on what the unit object is, this may
115 |   ||| or may not actually be useful.
116 |   |||
117 |   ||| The name comes from the fact that in the monoidal category of
118 |   ||| vector spaces, this takes a square matrix `M` to the 1x1 matrix
119 |   ||| `[ tr(M) ]`.
120 |   public export %inline
121 |   (.trace) : (rec : TracedR) -> {a : _} ->
122 |              rec.hom a a -> rec.hom rec.unit rec.unit
123 |   (.trace) rec = trace @{rec.impl}
124 |