[Agda] Decidable _\equiv_

[Sergei Meshveliani]

People,

I have the two questions on the declaration of

  module Foo {α α= α≤} 
             (dto  : DecTotalOrder α α= α≤)
             (_≡?_ : Decidable (_≡_ {A = DecTotalOrder.Carrier dto})))
             where
  ...


1. Is it possible here something like 
                  ...
                  (_≡?_ : let C = DecTotalOrder.Carrier dto
                          in  Decidable (_≡_ {A = C})
                  )
    ?

2. (As  dto  implies  Decidable _≈_),
   can this  _≡?_  be derived from  dto ?

   (I suspect that it cannot).

Thanks,

------
Sergei