Mercurial > hg > Papers > 2015 > atton-thesis

view src/delta_monad_in_agda.agda @ 45:12c5e455fe55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing description proofs of monad-laws for delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 10:33:47 +0900
parents
children
line wrap: on
line source

headDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S n) -> A
headDelta (mono x)    = x
headDelta (delta x _) = x

tailDelta : {l : Level} {A : Set l} {n : Nat} ->
    Delta A (S (S n)) -> Delta A (S n)
tailDelta (delta _ d) = d


delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n)
delta-eta {n = O}     x = mono x
delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x)

delta-mu : {l : Level} {A : Set l} {n : Nat} ->
           (Delta (Delta A (S n)) (S n)) -> Delta A (S n)
delta-mu (mono x)    = x
delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d))