[Agda] injectivity of Data.Char.toNat?

[Ramana Kumar]

Is the following provable? How?

foo₁ : (_≡_ on Data.Char.toNat) ⇒ _≡_
foo₁ = ?

foo₂ : _≡_ ⇒ (_≡_ on Data.Char.toNat)
foo₂ = PropEq.cong Data.Char.toNat

Could I combine the above two values to something that would enable a
strict total order on characters using _≡_ as the equality (rather
than (_≡_ on Data.Char.toNat))?