Mercurial > hg > Members > atton > agda-proofs
comparison sandbox/FunctorExample.agda @ 11:26e64661b969
Add example for Natural Transformation (head)
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 20 Jan 2015 13:35:12 +0900 |
parents | 7c7659d4521d |
children |
comparison
equal
deleted
inserted
replaced
10:7c7659d4521d | 11:26e64661b969 |
---|---|
126 ∎ | 126 ∎ |
127 | 127 |
128 concat-is-natural-transformation : {l : Level} -> NaturalTransformation (\A -> List (List A)) List | 128 concat-is-natural-transformation : {l : Level} -> NaturalTransformation (\A -> List (List A)) List |
129 {list-fmap ∙ list-fmap} {list-fmap {l}} concat | 129 {list-fmap ∙ list-fmap} {list-fmap {l}} concat |
130 concat-is-natural-transformation = record {commute = concat-commute} | 130 concat-is-natural-transformation = record {commute = concat-commute} |
131 | |
132 | |
133 data NonEmptyList {l : Level} (A : Set l) : Set l where | |
134 val : A -> NonEmptyList A | |
135 con : A -> NonEmptyList A -> NonEmptyList A | |
136 | |
137 head : {l : Level} {A : Set l} -> NonEmptyList A -> A | |
138 head (val x) = x | |
139 head (con x _) = x | |
140 | |
141 nel-fmap : {l : Level} {A B : Set l} -> (A -> B) -> NonEmptyList A -> NonEmptyList B | |
142 nel-fmap f (val x) = val (f x) | |
143 nel-fmap f (con x l) = con (f x) (nel-fmap f l) | |
144 | |
145 head-commute : {l : Level} {A B : Set l} -> (f : A -> B) (x : NonEmptyList A) -> head (nel-fmap f x) ≡ id f (head x) | |
146 head-commute f (val x) = refl | |
147 head-commute f (con x v) = refl | |
148 | |
149 head-is-nt : {l : Level} {A : Set l} -> NaturalTransformation {l} NonEmptyList id {nel-fmap} {id} head | |
150 head-is-nt = record { commute = head-commute } |