Slimming down `Data.Char`

[JacquesCarette]

Like with Data.Bool, this does

open import Data.Char.Properties
  using (_≈?_; _≟_; _<?_; _≤?_; _==_) public

where Data.Char.Properties has a large set of dependencies, but those few imports do not.

[MatthewDaggitt]

Most Data.X modules follow this pattern, not just Char and Bool. Only need one issue to discuss this design so I'm going to close this and let the discussion happen in #1487