Add List functor

1 files changed, 15 insertions, 0 deletions

diff --git a/Functor/Instance/Endo/List.agda b/Functor/Instance/Endo/List.agda
new file mode 100644
index 0000000..67e3d0b
--- /dev/null
+++ b/Functor/Instance/Endo/List.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Functor.Instance.Endo.List {ℓ : Level} where
+
+import Functor.Instance.List {ℓ} {ℓ} as List
+
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Endofunctor)
+
+-- List is only an endofunctor when the carrier sets and 
+-- equivalence relations live at the same level
+List : Endofunctor (Setoids ℓ ℓ)
+List = List.List