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 }