module Algebra.Functor
import Builtin
%default total
public export
interface Functor t where
  map : (a -> b) -> t a -> t b
  proofIdentity : (x : t a) -> map Builtin.identity x = x
  proofComposition : (f : a -> b) -> (g : b -> c) -> (x : t a) -> map (g . f) x = map g . map f $ x

import Algebra.Functor
%default total

public export
Functor Optional where
  map f Nothing  = Nothing
  map f (Some a) = Some . f $ a
  proofIdentity Nothing  = Refl
  proofIdentity (Some a) = Refl
  proofComposition f g Nothing  = Refl
  proofComposition f g (Some a) = Refl