Test.agda

module Test where

open import Function using (id ; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Data.Maybe

record RawFunctor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

open RawFunctor {{...}} public

record IsFunctor (F : Set → Set) {{R : RawFunctor F}} : Set₁ where
  field
    fmap-id :
      ∀ {A} → (x : F A) → fmap id x ≡ x
    fmap-combine :
      ∀ {A B C} (f : A → B) (g : B → C) (x : F A) →
        fmap g (fmap f x) ≡ fmap (g ∘ f) x
open IsFunctor {{...}} public


instance
  maybeRawFunctor : RawFunctor Maybe
  maybeRawFunctor = {!!}

  maybeIsFunctor : IsFunctor Maybe {{maybeRawFunctor}}
  maybeIsFunctor = {!!}

maybe-fmap-id : ∀ {A : Set} → (x : Maybe A) → fmap id x ≡ x
maybe-fmap-id x = fmap-id x