[Agda] How to formalize synonym types?

[Herminie Pagel]

Hi,

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`.

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.

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.

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?
Bool \bB : Dual
Dual ≡ ⊤
Nat \bN nat : Naturals
Naturals ≡ ⊤

Or maybe with an equivalence relationship, let`s say `≡-synonym`?
\bB ≡-synonym Bool
\bN ≡-synonym Nat
tt ≡-synonym True
cero ≡-synonym zero

Is there some definition about synonymity that may be available in the
standard library?

Thanks and happy new year you all.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191231/ab19d601/attachment.html>