[Agda] strict total order on characters

[Ramana Kumar]

I have three questions about the following snippet.

-----8<-----
open import Relation.Binary using () renaming (IsStrictTotalOrder to
ISTO;StrictTotalOrder to STO)
open import Data.Nat.Properties renaming (<-trans to N<-trans;
strictTotalOrder to Nsto)
import Data.Char
import Relation.Binary.On as RelOn

infix 4 _Char<_
_Char<_ : Rel Data.Char.Char _
_Char<_ = _N<_ on Data.Char.toNat

Char<-StrictTotalOrder = record
  { Carrier            = Data.Char.Char
  ; _≈_                = _≡_ on Data.Char.toNat
  ; _<_                = _Char<_
  ; isStrictTotalOrder = RelOn.isStrictTotalOrder Data.Char.toNat
(STO.isStrictTotalOrder Nsto)
  }
------8<-----

1. (How) Can I show that (_≡_ on Data.Char.toNat) is the same as _≡_?
Is there a hope of using the latter for the _≈_ field of the record?

2. Would code achieving the above not be appropriate for the standard
library? And (probably using it) an ordering on strings too?

3. Do you have any comments whatsoever on how to improve the style and
clarity (given that this was written by a novice)?

(4. the second last line was yellow for a while, but now it seems to
be loading fine... I think all I changed was the order in which I
opened/imported stuff...)