I assumed you could curry any function in Agda. So that you can always swap the order of the inputs.

and a theorem expressing that even compiles:

```
curry : {A : Set} -> {B : Set} -> {C : Set} -> ( A -> B -> C) -> (B -> A -> C)
curry f b a = f a b
```

However, Agda has dependent types and something like

```
curry' : {A : Set} -> {B : ( A -> Set ) } -> { C : ( A -> Set ) } -> ( (a : A) -> B a -> C a) -> ( B a -> (a : A) -> C a)
```

doesn't even compile.

Since `(a : A) -> B a -> C a`

is just as valid as `A -> B -> C`

I'm starting tho think that you cannot curry in general. Though nothing seems particularly awful about handing a function `B a`

before `a : A`

.

Is there some trick to perform currying in general? or is it not possible in Agda?