1 files changed, 58 insertions, 2 deletions
diff --git a/Structures.agda b/Structures.agda
index f1fd85b..10abd42 100644
--- a/Structures.agda
+++ b/Structures.agda
@@ -1,10 +1,17 @@
 module Structures where
 
 open import Category.Functor using (RawFunctor ; module RawFunctor)
-open import Function using (_∘_ ; id)
+open import Category.Monad using (module RawMonad)
+open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad)
+open import Data.Nat using (ℕ)
+open import Data.Vec as V using (Vec)
+import Data.Vec.Properties as VP
+open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)
+
+open import Generic using (sequenceV)
 
 record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
   field
@@ -29,3 +36,52 @@ record Functor (f : Set → Set) : Set₁ where
 
   open RawFunctor rawfunctor public
   open IsFunctor isFunctor public
+
+record IsShaped (S : Set)
+                (C : Set → S → Set)
+                (arity : S → ℕ)
+                (content : {α : Set} {s : S} → C α s → Vec α (arity s))
+                (fill : {α : Set} → (s : S) → Vec α (arity s) → C α s)
+                : Set₁ where
+  field
+    content-fill : {α : Set} {s : S} → (c : C α s) → fill s (content c) ≡ c
+    fill-content : {α : Set} → (s : S) → (v : Vec α (arity s)) → content (fill s v) ≡ v
+
+  fmap : {α β : Set} → (f : α → β) → {s : S} → C α s → C β s
+  fmap f {s} c = fill s (V.map f (content c))
+
+  isFunctor : (s : S) → IsFunctor (flip C s) (λ f → fmap f)
+  isFunctor s = record
+    { cong = λ g≗h c → P.cong (fill s) (VP.map-cong g≗h (content c))
+    ; identity = λ c → begin
+        fill s (V.map id (content c))
+          ≡⟨ P.cong (fill s) (VP.map-id (content c)) ⟩
+        fill s (content c)
+          ≡⟨ content-fill c ⟩
+        c ∎
+    ; composition = λ g h c → P.cong (fill s) (begin
+        V.map (g ∘ h) (content c)
+          ≡⟨ VP.map-∘ g h (content c) ⟩
+        V.map g (V.map h (content c))
+          ≡⟨ P.cong (V.map g) (P.sym (fill-content s (V.map h (content c)))) ⟩
+        V.map g (content (fill s (V.map h (content c)))) ∎)
+    } where open ≡-Reasoning
+
+  fmap-content : {α β : Set} → (f : α → β) → {s : S} → content {β} {s} ∘ fmap f ≗ V.map f ∘ content
+  fmap-content f c = fill-content _ (V.map f (content c))
+  fill-fmap : {α β : Set} → (f : α → β) → (s : S) → fmap f ∘ fill s ≗ fill s ∘ V.map f
+  fill-fmap f s v = P.cong (fill s ∘ V.map f) (fill-content s v)
+
+  sequence : {α : Set} {s : S} → C (Maybe α) s → Maybe (C α s)
+  sequence {s = s} c = fill s <$> sequenceV (content c)
+    where open RawMonad MaybeMonad
+
+record Shaped (S : Set) (C : Set → S → Set) : Set₁ where
+  field
+    arity : S → ℕ
+    content : {α : Set} {s : S} → C α s → Vec α (arity s)
+    fill : {α : Set} → (s : S) → Vec α (arity s) → C α s
+
+    isShaped : IsShaped S C arity content fill
+
+  open IsShaped isShaped public