Use sym-associator for Cats and DagCats

agda · May 29, 2024 · 23306c7 · 23306c7
1 parent d6b02c7
commit 23306c7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Categories/Category/Instance/Cats.agda b/src/Categories/Category/Instance/Cats.agda
@@ -9,7 +9,7 @@ open import Level
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
+  using (NaturalIsomorphism; associator; sym-associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_)
 private
   variable
     o ℓ e : Level
@@ -24,7 +24,7 @@ Cats o ℓ e = record
   ; id        = id
   ; _∘_       = _∘F_
   ; assoc     = λ {_ _ _ _ F G H} → associator F G H
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator F G H
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²

diff --git a/src/Categories/Category/Instance/DagCats.agda b/src/Categories/Category/Instance/DagCats.agda
@@ -18,7 +18,7 @@ DagCats o ℓ e = record
   ; id = id
   ; _∘_ = _∘F†_
   ; assoc = λ {_ _ _ _ F G H} → associator (functor F) (functor G) (functor H)
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator (functor F) (functor G) (functor H))
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator (functor F) (functor G) (functor H)
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²