1 files changed, 31 insertions, 0 deletions
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