Identity functor and monad laws

Id.agda

module Id where

open import Relation.Binary.PropositionalEquality.Core
open import Function

data Id : Set → Set where
  Itself : ∀{A} → A → Id A

fmap : ∀{A B} → (A → B) → Id A → Id B
fmap f (Itself x) = Itself (f x)

pure : ∀{A} → A -> Id A
pure x = Itself x

infixr 5 _>>=_

_>>=_ : ∀{A B} → Id A → (A -> Id B) -> Id B
Itself x >>= f = f x

functorIdentity : ∀{A} → (x : Id A) → fmap id x ≡ x
functorIdentity (Itself x) = refl

functorComposition : ∀{A B C}
                   → (x : Id A) → (g : A → B) → (f : B → C)
                   → fmap (f ∘ g) x ≡ fmap f (fmap g x)
functorComposition (Itself x) g f = refl

pureBind : ∀{A B} → (x : A) → (f : A → Id B) → pure x >>= f ≡ f x
pureBind x f = refl

bindPure : ∀{A} → (x : Id A) → x >>= pure ≡ x
bindPure (Itself x) = refl

bindAssoc : ∀{A B C} → (m : Id A) → (f : A → Id B) → (g : B → Id C)
          → m >>= (λ x → f x >>= g) ≡ (m >>= f) >>= g
bindAssoc (Itself x) f g = refl