<div dir="ltr">Hi,<br><br>I saw that the boolean datatype is sometimes named `Bool` but also `bool` or `\bB`. For the constructors is the same, sometimes referred to as `true` and `false` or `tt` and `ff`.<br><br>Also, the naturals receive the name `Nat` and `\nN`, among others. Its constructors are usually named `zero` and `suc`, but they could be called other names also, like `cero` and `sig` or `null` and `nae` or even completely invented names.<br><br>Intuitively, it seems clear that `Bool` and `\bB` express the same concept by looking at its declarations, as well as with `Nat` and `\nN`, but I do not know how this can be formalized.<br><br>Can it be done, e.g., by declaring a type, let`s say `Dual` or `Naturals` and then checking that synonymic datatypes belong to them and the new datatype has exactly one element?<br>Bool \bB : Dual<br>Dual ≡ ⊤<br>Nat \bN nat : Naturals<br>Naturals ≡ ⊤<br><br>Or maybe with an equivalence relationship, let`s say `≡-synonym`?<br>\bB ≡-synonym Bool<br><div>\bN ≡-synonym Nat</div><div>tt ≡-synonym True<br></div><div>cero ≡-synonym zero</div><div><br></div>Is there some definition about synonymity that may be available in the standard library?<br><br>Thanks and happy new year you all.</div>