Negation

• (a → b) → (¬b → ¬a) (“contrapositive law”)

     \f -> \nb -> \a -> nb (f a)
       :: (a -> b) -> (b -> Void) -> (a -> Void)

• (Actually Haskell will tell you this has type (a -> b) -> (b -> c) -> (a -> c))

• (But Void is an example of type c)

• ((a → (b ∨ c)) ∧ ¬c) → (a → b)

      \z -> let f  = fst z
                nc = snd z
             in \a -> case f a of 
                       Left b  -> b
                       Right c -> nc c
        :: (a -> Either b c, c -> Void) -> (a -> b)

      \z -> \a -> case fst z a of
                    Left b  -> b
                    Right c -> snd z c
        :: (a -> Either b c, c -> Void) -> (a -> b)