:PROPERTIES: :ID: 01d15593-0e51-4671-a652-c1a5fcfac81d :mtime: 20240111104545 :ctime: 20240111104543 :END: #+title: Maybe functor #+filetags: :public:project: * Definition of the Maybe Functor The Maybe functor is an [[id:57733bd2-5fa6-4615-9ab8-e50a4edd3f0b][endofunctor]] on the [[id:6ac2146d-0b78-40f0-a546-9322e5f1e9f0][Category of Computable Functions]] (abbreviated as COM). 1) The maybe functor maps object $x$ in $COM$ to object $Just(x)$ in $COM$ 2) The maybe functor maps arrow $a \to b$ in $COM$ to the arrow $Maybe(a) \to Maybe(b)$ in $COM$ The maybe functor also observes the consistency conditions of a functor: 1) To see that the maybe functor respects identity, case split on the argument 2) To see that the maybe functor respects composition, case split on the argument * Maybe Functor in Agda #+BEGIN_SRC agda fmapMaybe : (a → b) → Maybe a → Maybe b fmapMaybe f Nothing = Nothing fmapMaybe f (Just x) = Just (f x) fmapId : {a : Type} → fmapMaybe {a = a} {b = a} (λ x → x) ≡ (λ x → x) fmapId i Nothing = Nothing fmapId i (Just x) = Just x ∘maybe : {a b c : Type} {f : a → b} {g : b → c} → fmapMaybe ((functionCat ≫ f) g) ≡ (functionCat ≫ fmapMaybe f) (fmapMaybe g) ∘maybe i Nothing = Nothing ∘maybe {f = f} {g = g} i (Just x) = Just (g (f x)) maybeFunctor : Functor functionCat functionCat maybeFunctor = record { Fₒ = Maybe ; Fₐ = fmapMaybe ; F-id = fmapId ; F-∘ = ∘maybe } #+END_SRC