{-# language TypeOperators, RankNTypes, LiberalTypeSynonyms, ImpredicativeTypes #-}

f :: p -> q

h :: q, feltéve, hogy f :: p
----------------------------
     \f -> h :: p -> q

h :: p -> q     f :: p
----------------------
      h f :: q

la :: p -> p
la = \h -> h

lb :: p -> q -> p
lb = \f g -> f

lb' :: (p -> q) -> p
lb' = undefined

type True = ()

() :: True

type False = forall p . p

fromFalse :: False -> a
fromFalse f = f

   h :: False
----------------
fromFalse h :: p

lc :: (p -> False) -> p -> q
lc f g = fromFalse (f g)

type p :/\ q = (p, q)

h :: p     f :: q
-----------------
(h, f) :: p :/\ q

h :: p :/\ q   h :: p :/\ q
------------   ------------
 fst h :: p     snd h :: q

ld :: ((p -> q) :/\ (q -> r)) -> (p -> r)
ld = \h -> \f -> (snd h (fst h f))

le :: ((p :/\ q) :/\ r) -> (p :/\ (q :/\ r))
le = \h -> (fst (fst h), (snd (fst h), snd h))

type p :\/ q = Either p q

      h :: p             h :: q     
-----------------  ------------------
Left h :: p :\/ q  Right h :: p :\/ q

h :: p -> r    f :: q -> r
--------------------------
either h f :: p :\/ q -> r

lf :: (p :/\ q) :\/ r -> (p :\/ r) :/\ (q :\/ r)
lf (Left (f, h)) = (Left f, Left h)
lf (Right f) = (Right f, Right f)

lg :: q :\/ q -> q
lg (Left f) = f
lg (Right f) = f

type Not p = p -> False

lh :: Not (p :/\ Not p)
lh = \(p, np) -> np p

type p :<-> q = ((p -> q), (q -> p))

li :: (b :\/ a) :<-> (a :\/ b)
li = (either Right Left, either Right Left)

l2 :: (p -> q -> r) -> (q -> p -> r)
l2 = undefined

l3 :: p :<-> (True :/\ p)
l3 = undefined

l4 :: p :<-> (False :\/ p)
l4 = undefined

l5 :: (p -> q :/\ r) :<-> ((p -> q) :/\ (p -> r))
l5 = undefined

l6 :: (p :\/ q -> r) :<-> ((p -> r) :/\ (q -> r))
l6 = undefined

l7 :: p -> Not (Not p)
l7 = undefined

l8 :: Not (Not (p :\/ Not p))
l8 = undefined

l9 :: Not (Not (Not (Not p) -> p))
l9 = undefined

l10 :: Not (Not (Not p)) :<-> Not p
l10 = undefined

l11 :: Not (p :<-> Not p)
l11 = undefined

l12 :: (Not p :\/ q) -> (p -> q)
l12 = undefined

l13 :: (Not (p :\/ q)) :<-> (Not p :/\ Not q)
l13 = undefined

l14 :: (Not p :\/ Not q) -> Not (p :/\ q)
l14 = undefined

l15 :: Not (p :/\ q) -> (Not p :\/ Not q)
l15 = undefined