add a Functor structure
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Mar 2014 14:18:24 +0000 (15:18 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Mar 2014 14:27:32 +0000 (15:27 +0100)
commit3616445f9a60402701ca00a22e9e6e2fbe95c741
tree5dfc884e740a96b0b9615173fbce361f3c5ac25f
parent0041fbe99eab12df177e877bd5fe8d2f6fce9b0d
add a Functor structure

The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because

 * Other standard library structures in Algebra.Structures also require
   congruence.
 * Otherwise the identity law would have to reason about different
   identities.
Everything.agda
Structures.agda [new file with mode: 0644]