Q:

How can I store a function inside record/data type in Agda?

I've read the doc. It says:

The strict positivity condition rules out declarations such as
data Bad : Set where
    bad : (Bad → Bad) → Bad
    --     A     B      C
    -- A is in a negative position, B and C are OK

since there is a negative occurrence of Bad in the type of the argument of the constructor. (Note that the corresponding data type declaration of Bad is allowed in standard functional languages such as Haskell and ML.).

But it didn't say if there's an alternative way to store a function inside something else (like a data type or a record type).
I've also tried this, which does not compile as well:
bin-op : ∀ {ℓ} (A : Set ℓ) → Set ℓ
bin-op A = A → A → A

record Storer {ℓ} (A : Set ℓ) : Set where
  field
    operator : bin-op A

So how can I store a function inside a data type/record type/something else I don't know?

A:

The problem is in the
record Storer {ℓ} (A : Set ℓ) : Set where

part. Here you state that Storer belongs to the Set universe, however Storer contains bin-op A which is in the Set ℓ universe, and a record can't be smaller than its fields. Hence the fix is to define Storer to be in Set ℓ:
record Storer {ℓ} (A : Set ℓ) : Set ℓ where

Strict positivity is completely unrelated to the problem.
Universe polymorphism in Agda is described in the old wiki.

