Mercurial > hg > Papers > 2015 > atton-thesis
annotate src/delta_covariant.agda @ 50:37a832dff044
Add DeltaM example
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Feb 2015 17:56:51 +0900 (2015-02-15) |
parents | 4cc65012412f |
children |
rev | line source |
---|---|
42
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 delta-covariant : {l : Level} {n : Nat} {A B C : Set l} -> |
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 (f : B -> C) -> (g : A -> B) -> (d : Delta A (S n)) -> |
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d |
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 delta-covariant f g (mono x) = refl |
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 delta-covariant f g (delta x d) = cong (delta (f (g x))) |
4cc65012412f
Add proofs of functor-laws on delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 (delta-covariant f g d) |