Test.agda

module Test where

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

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

open RawFunctor {{...}} public

record Functor (F : Set → Set) : Set₁ where
  field
    raw : RawFunctor F
    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 Functor {{...}} hiding (raw) public