Mercurial > hg > Papers > 2015 > atton-thesis

annotate src/delta_left_unity_law.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-left-unity-law : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 (delta-mu ∙ (delta-fmap 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-left-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-left-unity-law {n = (S n)} (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-fmap delta-eta) (delta x d) ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ 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 (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ 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 (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 delta x d ≡⟨ refl ⟩
12c5e455fe55 Writing description proofs of monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 id (delta x d) ∎