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.

1 files changed, 1 insertions, 0 deletions

diff --git a/Everything.agda b/Everything.agda
index e37c76e..7383dd5 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,6 +2,7 @@
 module Everything where
 
 import Generic
+import Structures
 import FinMap
 import CheckInsert
 import GetTypes