[Agda] withdraw AVL ≈ request?

[Sergei Meshveliani]

People,
Earlier I asked a couple of times about generalizing  AVL
(binary tree table) from syntactic equality to a definitional one.

I have thought once more about the subject, and now doubt of whether
this request has sense. 

Because to use a generalized ALV Tree, one still needs to have the
following.
(1) To define  StrictTotalOrder _≈_ _<_  on  A = Key. 
(2) Most often it is done by defining a _canonical form_ map on A for
_≈_  and some DecTotalOrder  _<_ on canonical forms,  where  _<_  is
often set only for the purpose of a search by key.  

(for any reasonable computation domain it is really possible to define
(1) and (2), if one really cares for AVL). 

And it occurs that (1) and (2) give a map to a key domain Key' where
Key' can be used with _≡_ and _<_.
So, to use AVL of lib-0.7, one needs to add to one's `classes' such
operations as  canonical-form-as-key, _<_-as-key, key-StrictTotalOrder,
and to define them for each appropriate class instance. 
For example, having such for  A and B,  one can define such for  
A \times B,  and for  List A.

Probably the above AVL generalization will not make it any easier the
approach with (1) and (2) and defining instances.

There remains a certain point.
Having a canonical map to  Key', one could think of using some default
built-in  (_>_ , sto : StrictTotalOrder _≡_ _<_),

because it usually needs effort to invent this _<_.

As I recall, the Haskell library has such (do not recall of whether it
is on Standard).
The question is: whether Agda library could have such.

Regards,

------
Sergei