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

open import NeilPrelude

module Pointed (F : Set → Set)

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

-- 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

import Functor
open Functor F fmap 1stLaw 2ndLaw public