[Agda] Semigroup.Carrier in 2.3.2

[Serge D. Mechveliani]

People,
this program is accepted in by Agda-2.3.0.1 
and rejected by                Agda-2.3.2 :

---------------------------------------------------------------
powerToPositive : {c l : Level} -> {H : Semigroup c l} ->
            let C = Semigroup.Carrier H in  C -> (e : Nat) -> e > 0 -> C
--      
-- Power  x  to a positive degree  e.  The binary method.      

powerToPositive x e e>0 =  pow e e e>0
     where
     open Semigroup {{...}}
     pow : Nat -> (e : Nat) -> e > 0 -> Carrier
        -- cnt  is the counter used in termination proof  

     pow 0         _             _  = x
     pow _         0             ()
     pow _         (suc 0)       _  = x
     pow (suc cnt) (suc (suc e)) _  =
                              (if even? e then  p * p  else (p * p) * x)
                              where
                              half = suc $ quot2 e
                              p    = pow cnt half $ positiveHalf? e
---------------------------------------------------------------

Here I use the denotation (for this letter):
 \bn --> Nat,   
 \.  --> *,
 \~~ --> ~~ 
 \_1 --> _1   
 quot2 : Nat -> Nat   the integer part of quotient by 2, 
 positiveHalf?        a certain user function.

Agda-2.3.2  reports

-------------------------------
...
No variable of type
Semigroup
(_c_226 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
 e)
(_l_227 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
 e)
was found in scope.
when checking that the expression Carrier has type
Set
(_225 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
 e_1)
-------------------------------

Which is more correct, Agda-2.3.0.1 or Agda-2.3.2 ?
How to fix?

Also there is a question about  Standard library :
does it remain  lib-0.6 ?

My program  Main.agda  imports  lib-0.6,  and I use the same sources
of  lib-0.6 as under  Agda-2.3.0.1яя.
Now, when   Agda-2.3.2  compiles  Main.agda,
it type-checks and compiles all the modules in  lib-0.6  which are 
are needed for the import in  Main.agda,
right?

Thanks,

------
Sergei