# Quest 2 - Side Quests

## A Tautology / Currying / Cartesian Closed

In this side quest, you will construct the following functions.

```
uncurry : (A → B → C) → (A × B → C)
uncurry f x = {!!}
curry : (A × B → C) → (A → B → C)
curry f a b = {!!}
```

These have interpretations :

`uncurry`

is a proof that “if`A`

implies (`B`

implies`C`

)”, then “(`A`

and`B`

) implies`C`

”. A proof of the converse is`curry`

.this is a commonly occurring example of an

*adjunction*. See here for a more detailed explanation.

Note that we have *postulated* the types `A, B, C`

for you.

```
private
postulate
A B C : Type
```

In general, you can use this to
introduce new constants to your `agda`

file.
The `private`

ensures `A, B, C`

can only be used
within this `agda`

file.

Tip

`agda`

is space-and-indentation sensitive,
i.e. the `private`

applies to anything beneath it
that is indented two spaces.