The very rough sketch of this proof is as follows. First we use uniformity to show that an
α:−⇒Maybe(−) must “
act the same” on a
set X as it does on the singleton
set 1, entailing that
αX must either be always
Nothing or never
Nothing. Then we use uniformity to show that
α must “
act the same” on different
sets, entailing that it must be either always
Nothing for all sets or never
Nothing for all sets. Finally we use uniformity to show, similarly to the identity case, that if
α is never
Nothing then it must be
x↦Just(x).
Let
α be a uniform transformation
−⇒Maybe(−).
Let
X be a
set.
Choose
x0∈X and consider the pair
(t,u) consisting of
t:1→X, ⋆↦x0u:X→{star}, x↦⋆
where
1={⋆}. Uniformity of
α entails that
α1=t ; αX ; u∗
applying
⋆ to both sides and simplifying gives
α1(⋆)={NothingJust(⋆)αX(x0)=NothingαX(x0)=Nothing
Hence if
αX(x0)=Nothing then
α1 is constantly nothing, and otherwise is never nothing.
Since this holds for
all choices of
x0∈X, this means that
αX also must be either always
Nothing or never
Nothing. For if we had
x0,x1∈X with
αX(x0)=Nothing but
αX(x1)=Nothing, then
x0 would
witness that
α1 is always
Nothing and, contradictorily,
x1 would
witness that
α1 is never
Nothing.
Hence
αX is either always
Nothing or never
Nothing.
Further, it is the same regardless of choice of
X. Let
X1,X2 be
sets; WLOG let
X2 be at
least as large as
X1 so that exists a
function t:X1→X2 with post-inverse
u. If
αX2 were always nothing, then by uniformity we get
αX1=t ; αX2 ; u∗=x↦Nothing
In a similar way, if
αX2 were never nothing, uniformity entails that
αX1 also can never be
Nothing.
Thus
α is either always
Nothing for all X, or never
Nothing for all X.
Finally we strengthen “always
Nothing" and “never
Nothing" to particular mappings.
If
α is always
Nothing then it is the constant mapping
x↦Nothing
If
α is never
Nothing then it is of the form
αX(x)=Just(fX(x)) for some
f. Uniformity of
α entails uniformity of
f (the details of this are uninteresting), which means that
f:−⇒− must be the identity. Hence
αX is the mapping
x↦Just(x).
Therefore any uniform mapping
α:−⇒Maybe(−) is either the mapping
x↦Nothing or the mapping
x↦Just(x).