{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude

module Functor (F : Set → Set)

       (fmap'         : {A B : Set} → (A → B) → F A → F B)

-- Functor Laws
       
       (1stLaw : {A : Set} → {fa : F A} → Extensionality → fmap' id fa ≡ fa)

       (2ndLaw : {A B C : Set} → {f : A → B} → {g : B → C} → {fa : F A} → Extensionality
                 → fmap' (g ∘ f) fa ≡ (fmap' g ∘ fmap' f) fa)

where

fmap : {A B : Set} → (A → B) → F A → F B
fmap = fmap'

fmapId : {A : Set} → {fa : F A} → Extensionality → fmap id fa ≡ fa
fmapId = 1stLaw

fmapId' : {A : Set} → Extensionality → fmap {A} id ≡ id
fmapId' ext = ext (λ _ → fmapId ext)


naturality : {A B C : Set} → {f : A → B} → {g : B → C} → {fa : F A} → Extensionality → fmap (g ∘ f) fa ≡ (fmap g ∘ fmap f) fa
naturality = 2ndLaw

naturality' : {A B C : Set} → {f : A → B} → {g : B → C} → Extensionality → fmap (g ∘ f) ≡ fmap g ∘ fmap f
naturality' ext = ext (λ _ → 2ndLaw ext)