Axioms.hs

module Axioms where

import Prelude (const, undefined)

newtype Void = Void Void
data Prod a b = Prod a b
data Sum a b = A1 a | A2 b

a1 :: a -> (b -> a)
a1 a b = a

a2 :: (a -> b) -> ((b -> c) -> (a -> c))
a2 f g x = g (f x)

a3 :: a -> (b -> (a,b))
a3 a b = (a,b)

a4 :: Prod a b -> a
a4 (Prod a _) = a

a5 :: Prod a b -> b
a5 (Prod _ b) = b

a6 :: a -> Sum a b
a6 a = A1 a

a7 :: b -> Sum a b
a7 b = A2 b

a8 :: (a -> c) -> ((b -> c) -> ((Sum a b) -> c))
a8 f g x =
  let res (A1 a) = f a
      res (A2 b) = g b
  in res x

a9 :: (a -> b) -> (a -> (b -> Void)) -> (a -> Void)
a9 f g x = g x (f x)

-- ???
a10 :: a -> ((a -> Void) -> b)
a10 a f = const undefined (f a)

mp :: (a, a -> b) -> b
mp (x, f) = f x