Added to IO.agda

I added a few more IO functions (namely `putChar`, `readChar`, and `readLine`) to `IO.Primitive` and `IO`. These are pretty self-explanatory.

I also added the utility functions `_>>♯_` and `_>>=♯_` to `IO`. These allow ∞ IO objects to be "chained" together. Basically, they are like `_>>_` and `_>>=_` respectively, but they evaluate to values of type `∀ {a} {A : set a} -> ∞ (IO A)`.

Together, these additions allow one to write the program:

    open import Coinduction
    open import Data.Char
    open import Data.String
    open import Data.Unit
    open import IO
    
    agdaMain : ∞ (IO ⊤)
    agdaMain =
      ♯ putStrLn "Enter a string..." >>♯
      ♯ getLine >>=♯ λ str →
      ♯ putStrLn ("You entered " ++ str) >>♯
      ♯ putStrLn "Enter a character..." >>♯
      ♯ getChar >>=♯ λ c →
      ♯ putStr "You entered " >>♯
      ♯ putChar c >>♯
      ♯ putChar '\n'
    
    main = run (♭ agdaMain)

All without having to go through IO.Primitive or the ffi.