From e6473296bed95272061bb0903bdf4dd38011bed4 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 29 Oct 2025 19:45:10 -0500
Subject: Add List functor

---
 Functor/Instance/Endo/List.agda | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 Functor/Instance/Endo/List.agda

(limited to 'Functor/Instance/Endo/List.agda')

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
-- 
cgit v1.2.3