Mercurial > hg > Papers > 2015 > atton-thesis

annotate src/delta_right_unity_law.agda @ 56:398b42a1ac19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix layouts
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 16 Feb 2015 15:05:11 +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-right-unity-law : {l : Level} {A : 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 (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 delta-right-unity-law (mono x) = refl
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 delta-right-unity-law (delta x d) = begin
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 (delta-mu ∙ delta-eta) (delta x d)
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 delta-mu (delta-eta (delta x d))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 delta-mu (delta (delta x d) (delta-eta (delta x d)))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt tailDelta (delta x d))) ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 delta x (delta-mu (delta-eta (tailDelta (delta x d))))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 delta x (delta-mu (delta-eta d))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 delta x d
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 id (delta x d) ∎