From a34e05e875802477f8794ecb330b01c473c024c4 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 30 Oct 2025 17:20:33 -0500 Subject: Make list natural transformations level-polymorphic --- NaturalTransformation/Instance/EmptyList.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'NaturalTransformation/Instance/EmptyList.agda') 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) } -- cgit v1.2.3