### view agda/laws.agda @ 102:9c62373bd474

Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
author Yasutaka Higa Sun, 25 Jan 2015 12:16:34 +0900 f26a954cd068 a271f3ff1922
line wrap: on
line source
```
open import Relation.Binary.PropositionalEquality
open import Level
open import basic

module laws where

record Functor {l : Level} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where
field
fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
field
preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x
covariant   : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A)
-> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x

open Functor

record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')
{fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
{fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}
(natural-transformation : {A : Set l}  -> F A -> G A)
: Set (suc l) where
field
commute : {A B : Set l} -> (f : A -> B) -> (x : F A) ->
natural-transformation (fmapF f x) ≡  fmapG f (natural-transformation x)
open NaturalTransformation

-- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
record Monad {l : Level} {A : Set l}
(M : {ll : Level} -> Set ll -> Set ll)
(functorM : Functor {l} M)
: Set (suc l)  where
field -- category
mu  :  {A : Set l} -> M (M A) -> M A
eta :  {A : Set l} -> A -> M A