diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-03-07 15:18:24 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-03-07 15:27:32 +0100 |
| commit | 3616445f9a60402701ca00a22e9e6e2fbe95c741 (patch) | |
| tree | 5dfc884e740a96b0b9615173fbce361f3c5ac25f /Instances.agda | |
| parent | 0041fbe99eab12df177e877bd5fe8d2f6fce9b0d (diff) | |
| download | bidiragda-3616445f9a60402701ca00a22e9e6e2fbe95c741.tar.gz | |
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.
Diffstat (limited to 'Instances.agda')
0 files changed, 0 insertions, 0 deletions