### view agda/laws.agda @ 146:57601209eff3defaulttip

Add an example used multi types on Delta
author Yasutaka Higa Tue, 24 Mar 2015 17:04:00 +0900 575de2e38385
line wrap: on
line source

open import Relation.Binary.PropositionalEquality
open import Level

open import basic

module laws where

record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where
field
fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
field -- laws
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
field -- proof assistant
fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx
open Functor

record NaturalTransformation {l : Level} (F G : 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

record Monad {l : Level} (T : Set l -> Set l) (F : Functor T) : Set (suc l)  where
field -- category
mu  :  {A : Set l} -> T (T A) -> T A
eta :  {A : Set l} -> A -> T A
field -- natural transformations
eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A)       -> (eta ∙ f) x ≡ fmap F f (eta x)
mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) -> mu (fmap F (fmap F f) x) ≡ fmap F f (mu x)
field -- category laws
association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu))  x ≡ (mu ∙ mu) x
right-unity-law  : {A : Set l} -> (x : T A)           -> (mu ∙ (fmap F eta)) x ≡ id x
left-unity-law : {A : Set l} -> (x : T A)           -> id x ≡ (mu ∙ eta) x