replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicate
[~helmut/bidiragda.git] / Structures.agda
1 module Structures where
2
3 open import Category.Functor using (RawFunctor ; module RawFunctor)
4 open import Category.Monad using (module RawMonad)
5 open import Data.Maybe using (Maybe)
6 open import Data.Maybe.Categorical using () renaming (monad to MaybeMonad)
7 open import Data.Nat using (ℕ)
8 open import Data.Vec as V using (Vec)
9 import Data.Vec.Properties as VP
10 open import Function using (_∘_ ; flip ; id)
11 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
12 open import Relation.Binary using (_Preserves_⟶_)
13 open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; module ≡-Reasoning)
14
15 open import Generic using (sequenceV)
16
17 record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
18   field
19     cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
20     identity : {α : Set} → f {α} id ≗ id
21     composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
22                   f (g ∘ h) ≗ f g ∘ f h
23
24   isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
25   isCongruence {α} {β} = record
26     { _⟨$⟩_ = λ g → record
27       { _⟨$⟩_ = f (_⟨$⟩_ g)
28       ; cong = P.cong (f (_⟨$⟩_ g))
29       }
30     ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h P.refl) x)
31     }
32
33 record Functor (f : Set → Set) : Set₁ where
34   field
35     rawfunctor : RawFunctor f
36     isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)
37
38   open RawFunctor rawfunctor public
39   open IsFunctor isFunctor public
40
41 record IsShaped (S : Set)
42                 (C : Set → S → Set)
43                 (arity : S → ℕ)
44                 (content : {α : Set} {s : S} → C α s → Vec α (arity s))
45                 (fill : {α : Set} → (s : S) → Vec α (arity s) → C α s)
46                 : Set₁ where
47   field
48     content-fill : {α : Set} {s : S} → (c : C α s) → fill s (content c) ≡ c
49     fill-content : {α : Set} → (s : S) → (v : Vec α (arity s)) → content (fill s v) ≡ v
50
51   fmap : {α β : Set} → (f : α → β) → {s : S} → C α s → C β s
52   fmap f {s} c = fill s (V.map f (content c))
53
54   isFunctor : (s : S) → IsFunctor (flip C s) (λ f → fmap f)
55   isFunctor s = record
56     { cong = λ g≗h c → P.cong (fill s) (VP.map-cong g≗h (content c))
57     ; identity = λ c → begin
58         fill s (V.map id (content c))
59           ≡⟨ P.cong (fill s) (VP.map-id (content c)) ⟩
60         fill s (content c)
61           ≡⟨ content-fill c ⟩
62         c ∎
63     ; composition = λ g h c → P.cong (fill s) (begin
64         V.map (g ∘ h) (content c)
65           ≡⟨ VP.map-∘ g h (content c) ⟩
66         V.map g (V.map h (content c))
67           ≡⟨ P.cong (V.map g) (P.sym (fill-content s (V.map h (content c)))) ⟩
68         V.map g (content (fill s (V.map h (content c)))) ∎)
69     } where open ≡-Reasoning
70
71   fmap-content : {α β : Set} → (f : α → β) → {s : S} → content {β} {s} ∘ fmap f ≗ V.map f ∘ content
72   fmap-content f c = fill-content _ (V.map f (content c))
73   fill-fmap : {α β : Set} → (f : α → β) → (s : S) → fmap f ∘ fill s ≗ fill s ∘ V.map f
74   fill-fmap f s v = P.cong (fill s ∘ V.map f) (fill-content s v)
75
76   sequence : {α : Set} {s : S} → C (Maybe α) s → Maybe (C α s)
77   sequence {s = s} c = fill s <$> sequenceV (content c)
78     where open RawMonad MaybeMonad
79
80 record Shaped (S : Set) (C : Set → S → Set) : Set₁ where
81   field
82     arity : S → ℕ
83     content : {α : Set} {s : S} → C α s → Vec α (arity s)
84     fill : {α : Set} → (s : S) → Vec α (arity s) → C α s
85
86     isShaped : IsShaped S C arity content fill
87
88   open IsShaped isShaped public