diff --git a/src/Categories/Category/Instance/Cats.agda b/src/Categories/Category/Instance/Cats.agda
index 77b2ab8b..2a301910 100644
--- 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
index 8e8d8cf1..3f0fc654 100644
--- 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²