Make list natural transformations level-polymorphic

1 files changed, 5 insertions, 5 deletions

diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda
index 2164d6c..9a558a2 100644
--- a/NaturalTransformation/Instance/EmptyList.agda
+++ b/NaturalTransformation/Instance/EmptyList.agda
@@ -1,6 +1,8 @@
 {-# OPTIONS --without-K --safe #-}
 
-module NaturalTransformation.Instance.EmptyList where
+open import Level using (Level)
+
+module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where
 
 import Function.Construct.Constant as Const
 
@@ -8,10 +10,8 @@ open import Categories.NaturalTransformation using (NaturalTransformation; ntHel
 open import Categories.Functor using (Functor)
 open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Functor.Construction.Constant using (const)
-open import Data.List.Relation.Binary.Pointwise using (refl)
 open import Data.List using ([])
-open import Level using (0ℓ)
-open import Functor.Instance.List {0ℓ} {0ℓ} using (List)
+open import Functor.Instance.List {c} {ℓ} using (List)
 open import Relation.Binary using (Setoid)
 
 module List = Functor List
@@ -19,5 +19,5 @@ module List = Functor List
 ⊤⇒[] : NaturalTransformation (const SingletonSetoid) List
 ⊤⇒[] = ntHelper record
     { η = λ X → Const.function SingletonSetoid (List.₀ X) []
-    ; commute = λ {_} {B} f → let module B = Setoid B in refl B.refl
+    ; commute = λ {_} {B} f → Setoid.refl (List.₀ B)
     }