:PROPERTIES: :ID: d3daccd1-11e5-4f1b-bed0-2225988530a5 :mtime: 20240111104600 :ctime: 20240111104558 :END: #+title: list fuctor #+filetags: :public:project: * Definition of the List Functor The list functor in an [[id:57733bd2-5fa6-4615-9ab8-e50a4edd3f0b][endofunctor]] on [[id:6ac2146d-0b78-40f0-a546-9322e5f1e9f0][Category of Computable Functions]]. 1) the list functor maps an object $x$ in $COM$ to an object $List(x)$ in $COM$. 2) The list functor maps an arrow $a \to b$ in $COM$ to an arrow $List(a) \to List(b)$ in $COM$. The consistency conditions for a functor are satisfied 1) To see that the list functor respects identity, case split on the first argument. 2) To see that the list functor respects composition, case split on the first argument. * List Functor in Agda #+BEGIN_SRC agda data List (x : Type) : Type where [] : List x Cons : x → List x → List x fmapList : (a → b) → List a → List b fmapList f [] = [] fmapList f (Cons x xs) = Cons (f x) (fmapList f xs) fmapLID : {a : Type} → fmapList {a = a} {b = a} (λ x → x) ≡ λ x → x fmapLID _ [] = [] fmapLID i (Cons x xs) = Cons x (fmapLID i xs) ∘List : {a b c : Type} {f : a → b} {g : b → c} → fmapList ((functionCat ≫ f) g) ≡ (functionCat ≫ fmapList f) (fmapList g) ∘List i [] = [] ∘List {f = f} {g = g} i (Cons x xs) = Cons (g (f x)) (∘List {f = f} {g = g} i xs) listFunctor : Functor functionCat functionCat listFunctor = record { Fₒ = List ; Fₐ = fmapList ; F-id = fmapLID ; F-∘ = ∘List } #+END_SRC