We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 2648970 commit 52b1d3aCopy full SHA for 52b1d3a
src/Categories/Category/Monoidal/Traced.agda
@@ -12,14 +12,15 @@ open import Level
12
open import Data.Product using (_,_)
13
14
open import Categories.Category.Monoidal.Symmetric M
15
+open import Categories.Category.Monoidal.Reasoning M
16
17
private
18
variable
19
A B X Y : Obj
20
f g : A ⇒ B
21
22
------------------------------------------------------------------------------
--- Def from Traced monoidal categories (Joyal, Street, & Verity, 1994)
23
+-- Def from Traced monoidal categories (Joyal, Street, & Verity, 1996)
24
--
25
-- A symmetric monoidal category (C,⊗,1,b) (where b is the symmetry) is
26
-- said to be traced if it is equipped with a natural family of functions
0 commit comments