Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/functor.agda @ 126:5902b2a24abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 11:45:33 +0900
parents ee7f5162ec1f
children d205ff1e406f
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import basic
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import delta
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import delta.functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import deltaM
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
9 open import nat
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import laws
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 module deltaM.functor where
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
17 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
18 -> (d : DeltaM M A (S n)) -> deltaM-fmap id d ≡ id d
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
19 deltaM-preserve-id {F = F} (deltaM (mono x)) = begin
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
20 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
21 deltaM (fmap delta-is-functor (fmap F id) (mono x)) ≡⟨ refl ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
22 deltaM (mono (fmap F id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id F x) ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
23 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
24 deltaM (mono x) ∎
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
25 deltaM-preserve-id {F = F} (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
26 deltaM-fmap id (deltaM (delta x d))
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
27 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
28 deltaM (fmap delta-is-functor (fmap F id) (delta x d))
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
29 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
30 deltaM (delta (fmap F id x) (fmap delta-is-functor (fmap F id) d))
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
31 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap F id) d))) (preserve-id F x) ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
32 deltaM (delta x (fmap delta-is-functor (fmap F id) d))
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
33 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
34 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap F id) d))
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
35 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
36 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
37 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id {F = F} (deltaM d)) ⟩
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
38 appendDeltaM (deltaM (mono x)) (deltaM d)
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
39 ≡⟨ refl ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 deltaM (delta x d)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ∎
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
43
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
44 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat}
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
45 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
46 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M A (S n)) ->
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
47 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
48 deltaM-covariant {F = F} f g (deltaM (mono x)) = begin
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
49 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
50 deltaM (delta-fmap (fmap F (f ∙ g)) (mono x)) ≡⟨ refl ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
51 deltaM (mono (fmap F (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant F g f x) ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
52 deltaM (mono (((fmap F f) ∙ (fmap F g)) x)) ≡⟨ refl ⟩
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
53 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
54 deltaM-covariant {F = F} f g (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
55 deltaM-fmap (f ∙ g) (deltaM (delta x d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
56 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
57 deltaM (delta-fmap (fmap F (f ∙ g)) (delta x d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
58 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
59 deltaM (delta (fmap F (f ∙ g) x) (delta-fmap (fmap F (f ∙ g)) d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
60 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
61 appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM (delta-fmap (fmap F (f ∙ g)) d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
62 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
63 appendDeltaM (deltaM (mono (fmap F (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
64 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant F g f x) ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
65 appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
66 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
67 appendDeltaM (deltaM (mono (((fmap F f) ∙ (fmap F g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
68 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
69 appendDeltaM (deltaM (delta-fmap ((fmap F f) ∙ (fmap F g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
70 ≡⟨ refl ⟩
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
71 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
72 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) de) (deltaM-covariant {F = F} f g (deltaM d)) ⟩
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
73 appendDeltaM (deltaM ((((delta-fmap (fmap F f)) ∙ (delta-fmap (fmap F g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
74 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
75 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
76 ∎
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
77
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
78 deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
79 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
80 {f g : A -> B}
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
81 (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) ->
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
82 deltaM-fmap f d ≡ deltaM-fmap g d
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
83 deltaM-fmap-equiv {l} {A} {B} {O} {T} {F} {M} {f} {g} eq (deltaM (mono x)) = begin
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
84 deltaM-fmap f (deltaM (mono x)) ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
85 deltaM (mono (fmap F f x)) ≡⟨ cong (\de -> deltaM (mono de)) (fmap-equiv F eq x) ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
86 deltaM (mono (fmap F g x)) ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
87 deltaM-fmap g (deltaM (mono x))
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
88 ∎
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
89 deltaM-fmap-equiv {l} {A} {B} {S n} {T} {F} {M} {f} {g} eq (deltaM (delta x d)) = begin
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
90 deltaM-fmap f (deltaM (delta x d)) ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
91 deltaM (delta (fmap F f x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta de (delta-fmap (fmap F f) d))) (fmap-equiv F eq x) ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
92 deltaM (delta (fmap F g x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta (fmap F g x) de)) (delta-fmap-equiv (fmap-equiv F eq) d) ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
93 deltaM (delta (fmap F g x) (delta-fmap (fmap F g) d)) ≡⟨ refl ⟩
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
94 deltaM-fmap g (deltaM (delta x d))
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
95 ∎
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
96
113
47f144540d51 Delte trying code
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
97
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
98
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
99 deltaM-is-functor : {l : Level} {n : Nat}
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
100 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
101 Functor {l} (\A -> DeltaM M A (S n))
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
102 deltaM-is-functor {F = F} = record { fmap = deltaM-fmap
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
103 ; preserve-id = deltaM-preserve-id {F = F}
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
104 ; covariant = (\f g -> deltaM-covariant {F = F} g f)
126
5902b2a24abf Prove mu-is-nt for DeltaM with fmap-equiv
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
105 ; fmap-equiv = deltaM-fmap-equiv
123
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
106 }
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
107
ee7f5162ec1f Fix proof functor for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
108