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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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)