blob: 67e3d0ba5919c98392da0bce496896c05462e907 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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
|
