title: Agda Store Comonad
body: <p>I'm just starting with Agda but know some Haskell and would like to know how to define the Store Comonad in Agda.</p>
  <p>This is what I have until now:</p>
  <pre><code>   open import Category.Comonad
     open import Data.Product
  
     Store : Set → Set → ((Set → Set) × Set)
     Store s a = ((λ s → a) , s)
  
     StoreComonad : RawComonad (λ s a → (Store s a))
     StoreComonad = record
       { extract (Store s a) = extract s a
       ; extend f (Store s a = Store (extend (λ s' a' →­ f (Store s' a')) s) a
       } where open RawComonad
  </code></pre>
  <p>For now I'm getting the following error:</p>
  <pre><code>Parse error
  =&lt;ERROR&gt;
   extract s a
    ; extend f (Sto...
  </code></pre>
  <p>I'm not too sure what it is I'm doing wrong. Any help would be appreciated! Thanks!</p>
  <p><strong>EDIT</strong></p>
  <p>I think I'm getting closer. I replaced the fields in the record using matching lambdas:</p>
  <pre><code>Store : Set → Set → ((Set → Set) × Set)
  Store s a = ((λ s → a) , s)
  
  StoreComonad : RawComonad (λ s a → (Store s a))
  StoreComonad = record
    { extract   = λ st → (proj₁ st) (proj₂ st)
    ; duplicate = λ st → Store (λ s → Store (proj₁ st) s) (proj₂ st)
    ; extend    = λ g st → g (duplicate st)
    } where open RawComonad
  </code></pre>
  <p><code>RawComonad</code> is from <a href="https://github.com/agda/agda-stdlib/blob/master/src/Category/Comonad.agda" rel="nofollow noreferrer">https://github.com/agda/agda-stdlib/blob/master/src/Category/Comonad.agda</a>
  and has the signature</p>
  <pre><code>record RawComonad (W : Set f → Set f) : Set (suc f)
  </code></pre>
  <p>and <code>Store</code> is based on <code>type Store s a = (s -&gt; a, s)</code> in Haskell.</p>
  <p>Now the error I'm getting is:</p>
  <pre><code>(a : Set) → Σ (Set → Set) (λ x → Set) !=&lt; Set
  when checking that the expression λ a → Store s a has type Set
  </code></pre>
  <p>I'm wondering if this error has to do with this line:</p>
  <pre><code>StoreComonad : RawComonad (λ s a → (Store s a))
  </code></pre>
  <p>I find that the compilation error messages in Agda don't give many clues or I haven't yet been able to understand them well.</p>