[Agda] `let' in record decl

[Serge D. Mechveliani]

Please, how to abbreviate  `Carrier ord'  in the declaration  of
------------------------------------
record Merge1
  {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2)
  (m : Carrier ord) (xs : List $ Carrier ord) (ys : List $ Carrier ord)
                                        : Set (suc $ max c $ max l1 l2)
  where
  A = Carrier ord
  field list    : List A                     
        ordered : OrderedList? ord (m :: list)
------------------------------------
?
(Agda-2.3.0.1, MAlonzo).

After `where', it works  `A = Carrier ord'.
But how to abbreviate the previous three occurences?

Question 2.
(suc $ max c $ max l1 l2) : Level   
comes from my declaration of the type  OrderedList?
-- where this expression is copied from  DecTotalOrder 
(of Standard Library lib-0.6), without understanding of how the levels
must be set.
Now, what level needs to be set for  record Merge1  ?

Thank you in advance for explanation,

-------
Sergei