Default implementations of not and implies

[clayrat]

These should be mutually interdefinable:

  not : a -> a
  not x = x `implies` bottom
  implies : a -> a -> a
  implies x y = (not x) `join` y

[Risto-Stevcev]

Added it, thanks for the contrib 👍

[edrx]

  I don't quite understand the context that you are discussing, but
  here is a simple situation in which (not p) `join` q = p `implies` q
  is false.

  In this Heyting Algebra

        23  
      22  13
    21  12
  20  11  02
    10  01
      00

  if p = 20 and q = 11 then:

    (not p)          = 02
    (not p) `join` q = 12
       p `implies` q = 13

  Take a look at 
  http://angg.twu.net/LATEX/2017planar-has-1.pdf
  http://angg.twu.net/math-b.html#zhas-for-children-2
  for details.

[Risto-Stevcev]

Yeah you're right -- heyting algebras don't necessarily satisfy the law of excluded middle, I'm not sure why I accepted this change. I'll fix it

[Risto-Stevcev]

122489e