Mercurial > hg > Members > atton > agda-proofs
annotate sandbox/FunctorExample.agda @ 66:211fde284b7e
Trying prove n-push/n-pop
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Jan 2017 02:33:47 +0000 |
parents | 26e64661b969 |
children |
rev | line source |
---|---|
6 | 1 open import Level |
2 open import Relation.Binary.PropositionalEquality | |
3 open ≡-Reasoning | |
4 | |
5 | |
6 module FunctorExample where | |
7 | |
8 id : {l : Level} {A : Set l} -> A -> A | |
9 id x = x | |
10 | |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
11 _∙_ : {l : Level} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C) |
6 | 12 f ∙ g = \x -> f (g x) |
13 | |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
14 record Functor {l : Level} {A : Set l} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
15 field |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
16 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
17 field |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
18 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
19 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
20 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
21 open Functor |
6 | 22 |
23 | |
24 | |
9
4a0841123810
fmap for nested functor without implicit level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
25 data List {l : Level} (A : Set l) : (Set l) where |
6 | 26 nil : List A |
27 cons : A -> List A -> List A | |
28 | |
29 list-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> List A -> List B | |
30 list-fmap f nil = nil | |
31 list-fmap f (cons x xs) = cons (f x) (list-fmap f xs) | |
32 | |
33 list-preserve-id : {l : Level} {A : Set l} -> (xs : List A) -> list-fmap id xs ≡ id xs | |
34 list-preserve-id nil = refl | |
35 list-preserve-id (cons x xs) = cong (\li -> cons x li) (list-preserve-id xs) | |
36 | |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
37 list-covariant : {l : Level} {A B C : Set l} -> |
6 | 38 (f : A -> B) → (g : B -> C) → (x : List A) → list-fmap (g ∙ f) x ≡ list-fmap g (list-fmap f x) |
39 list-covariant f g nil = refl | |
40 list-covariant f g (cons x xs) = cong (\li -> cons (g (f x)) li) (list-covariant f g xs) | |
41 | |
42 | |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
43 list-is-functor : {l : Level} {A : Set l}-> Functor {l} {A} List |
9
4a0841123810
fmap for nested functor without implicit level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
44 list-is-functor = record { fmap = list-fmap ; |
4a0841123810
fmap for nested functor without implicit level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
45 preserve-id = list-preserve-id ; |
4a0841123810
fmap for nested functor without implicit level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
46 covariant = list-covariant} |
6 | 47 |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
48 fmap-to-nest-list : {l : Level} {A B : Set l} |
8
a3509dbb9e49
Example for implicit-level functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
49 -> (A -> B) -> (List (List A)) -> (List (List B)) |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
50 fmap-to-nest-list {l} {A} {B} f xs = Functor.fmap (list-is-functor {l} {List A}) (Functor.fmap {l} {A} list-is-functor f) xs |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
51 |
9
4a0841123810
fmap for nested functor without implicit level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
8
diff
changeset
|
52 data Identity {l : Level} (A : Set l) : Set l where |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
53 identity : A -> Identity A |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
54 |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
55 identity-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> Identity A -> Identity B |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
56 identity-fmap f (identity a) = identity (f a) |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
57 |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
58 identity-preserve-id : {l : Level} {A : Set l} -> (x : Identity A) -> identity-fmap id x ≡ id x |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
59 identity-preserve-id (identity x) = refl |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
60 |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
61 identity-covariant : {l : Level} {A B C : Set l} |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
62 (f : A -> B) → (g : B -> C) → (x : Identity A) → identity-fmap (g ∙ f) x ≡ identity-fmap g (identity-fmap f x) |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
63 identity-covariant f g (identity x) = refl |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
64 |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
65 identity-is-functor : {l : Level} {A : Set l} -> Functor {l} {A} Identity |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
66 identity-is-functor {l} = record { fmap = identity-fmap {l}; |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
67 preserve-id = identity-preserve-id ; |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
68 covariant = identity-covariant } |
6 | 69 |
70 | |
71 | |
72 | |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
73 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
74 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
75 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
76 (natural-transformation : {A : Set l} -> F A -> G A) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
77 : Set (suc l) where |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
78 field |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
79 commute : {A B : Set l} -> (f : A -> B) -> (x : F A) -> |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
80 natural-transformation (fmapF f x) ≡ fmapG f (natural-transformation x) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
81 open NaturalTransformation |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
82 |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
83 tail : {l : Level} {A : Set l} -> List A -> List A |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
84 tail nil = nil |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
85 tail (cons _ xs) = xs |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
86 |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
87 tail-commute : {l : Level} {A B : Set l} -> (f : A -> B) -> (xs : List A) -> |
7
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
88 tail (list-fmap f xs) ≡ list-fmap f (tail xs) |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
89 tail-commute f nil = refl |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
90 tail-commute f (cons x xs) = refl |
c11c259916b7
Example for natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
6
diff
changeset
|
91 |
10
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
92 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
93 tail-is-natural-transformation : {l : Level} -> NaturalTransformation List List {list-fmap} {list-fmap {l}} tail |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
94 tail-is-natural-transformation = record { commute = tail-commute} |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
95 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
96 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
97 append : {l : Level} {A : Set l} -> List A -> List A -> List A |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
98 append nil ys = ys |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
99 append (cons x xs) ys = cons x (append xs ys) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
100 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
101 append-with-fmap : {l : Level} {A B : Set l} -> (f : A -> B) -> (xs : List A) -> (ys : List A) -> |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
102 append (list-fmap f xs) (list-fmap f ys) ≡ list-fmap f (append xs ys) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
103 append-with-fmap f nil ys = refl |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
104 append-with-fmap f (cons x xs) ys = begin |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
105 append (list-fmap f (cons x xs)) (list-fmap f ys) ≡⟨ refl ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
106 append (cons (f x) (list-fmap f xs)) (list-fmap f ys) ≡⟨ refl ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
107 cons (f x) (append (list-fmap f xs) (list-fmap f ys)) ≡⟨ cong (\li -> cons (f x) li) (append-with-fmap f xs ys) ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
108 list-fmap f (append (cons x xs) ys) ∎ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
109 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
110 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
111 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
112 concat : {l : Level} {A : Set l} -> List (List A) -> List A |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
113 concat nil = nil |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
114 concat (cons x xs) = append x (concat xs) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
115 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
116 concat-commute : {l : Level} {A B : Set l} -> (f : A -> B) -> (xs : List (List A)) -> |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
117 concat ((list-fmap ∙ list-fmap) f xs) ≡ list-fmap f (concat xs) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
118 concat-commute f nil = refl |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
119 concat-commute f (cons x xs) = begin |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
120 concat ((list-fmap ∙ list-fmap) f (cons x xs)) ≡⟨ refl ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
121 concat (cons (list-fmap f x) ((list-fmap ∙ list-fmap) f xs)) ≡⟨ refl ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
122 append (list-fmap f x) (concat ((list-fmap ∙ list-fmap) f xs)) ≡⟨ cong (\li -> append (list-fmap f x) li) (concat-commute f xs) ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
123 append (list-fmap f x) (list-fmap f (concat xs)) ≡⟨ append-with-fmap f x (concat xs) ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
124 list-fmap f (append x (concat xs)) ≡⟨ refl ⟩ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
125 list-fmap f (concat (cons x xs)) |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
126 ∎ |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
127 |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
128 concat-is-natural-transformation : {l : Level} -> NaturalTransformation (\A -> List (List A)) List |
7c7659d4521d
Improve NaturalTransformation definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
129 {list-fmap ∙ list-fmap} {list-fmap {l}} concat |
11
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
130 concat-is-natural-transformation = record {commute = concat-commute} |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
131 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
132 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
133 data NonEmptyList {l : Level} (A : Set l) : Set l where |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
134 val : A -> NonEmptyList A |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
135 con : A -> NonEmptyList A -> NonEmptyList A |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
136 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
137 head : {l : Level} {A : Set l} -> NonEmptyList A -> A |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
138 head (val x) = x |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
139 head (con x _) = x |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
140 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
141 nel-fmap : {l : Level} {A B : Set l} -> (A -> B) -> NonEmptyList A -> NonEmptyList B |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
142 nel-fmap f (val x) = val (f x) |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
143 nel-fmap f (con x l) = con (f x) (nel-fmap f l) |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
144 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
145 head-commute : {l : Level} {A B : Set l} -> (f : A -> B) (x : NonEmptyList A) -> head (nel-fmap f x) ≡ id f (head x) |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
146 head-commute f (val x) = refl |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
147 head-commute f (con x v) = refl |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
148 |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
149 head-is-nt : {l : Level} {A : Set l} -> NaturalTransformation {l} NonEmptyList id {nel-fmap} {id} head |
26e64661b969
Add example for Natural Transformation (head)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
150 head-is-nt = record { commute = head-commute } |