Maps between type aliases

Stream: mathlib4

[Violeta Hernández]

I'm wondering if there's a general naming convention for the names of maps α ≅ Alias α and Alias α ≅ α. For docs#Lex, we have docs#toLex and docs#ofLex. I've also come across docs#ArchimedeanOrder.of and docs#ArchimedeanOrder.val.

I've personally added docs#Nimber.toOrdinal and docs#Ordinal.toNimber as examples, but these names are a bit longer than I'd like, so I'd be happy to rename them.