Mercurial > hg > Papers > 2015 > atton-thesis

annotate src/delta_eta_is_nt.agda @ 57:5f0e13923cfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 16 Feb 2015 16:24:42 +0900
parents 12c5e455fe55
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
45
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 (f : A -> B) -> (x : A) ->
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 delta-eta-is-nt {n = O} f x = refl
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 delta-eta-is-nt {n = S n} f x = begin
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 (delta-eta ∙ f) x ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 delta-eta (f x) ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 delta (f x) (delta-eta (f x))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 delta-fmap f (delta-eta x) ∎