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.

• currying

• 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.