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.

2 files changed, 32 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
diff --git a/Structures.agda b/Structures.agda
new file mode 100644
index 0000000..f1fd85b
--- /dev/null
+++ b/Structures.agda
@@ -0,0 +1,31 @@
+module Structures where
+
+open import Category.Functor using (RawFunctor ; module RawFunctor)
+open import Function using (_∘_ ; id)
+open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
+open import Relation.Binary using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
+
+record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
+  field
+    cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
+    identity : {α : Set} → f {α} id ≗ id
+    composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
+                  f (g ∘ h) ≗ f g ∘ f h
+
+  isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
+  isCongruence {α} {β} = record
+    { _⟨$⟩_ = λ g → record
+      { _⟨$⟩_ = f (_⟨$⟩_ g)
+      ; cong = P.cong (f (_⟨$⟩_ g))
+      }
+    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
+    }
+
+record Functor (f : Set → Set) : Set₁ where
+  field
+    rawfunctor : RawFunctor f
+    isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)
+
+  open RawFunctor rawfunctor public
+  open IsFunctor isFunctor public