Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are.
What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like
theorem1 : T (1 - 1 == 0)
which is somewhat interestingly different from
theorem2 : 1 - 1 = 0
in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).
Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0]
I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.
Comments
Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom.
I love to look at unicode, but is it a pain to type it in practice, even given emacs?
Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are.
What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like
which is somewhat interestingly different from in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0]
[0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...
I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.