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 “ifA
implies (B
impliesC
)”, then “(A
andB
) impliesC
”. A proof of the converse iscurry
.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.