[Agda] Slow type-checking of records

[Sergei Meshveliani]

On Tue, 2016-03-08 at 18:32 +0900, Andreas Abel wrote:
> Folklore suggests that you can improve performance by defining your 
> record values via copattern matching and/or no-eta record types.
> 
> --Andreas
> 
> On 08.03.2016 00:50, Andreas Nuyts wrote:
> > [..]


Please, where are explained  copattern matching  and  no-eta record
types?

For example, Standard library declares

 record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infix 4 _≈_
   field
     Carrier          : Set c
     _≈_              : Rel Carrier ℓ
     isDecEquivalence : IsDecEquivalence _≈_

   open IsDecEquivalence isDecEquivalence public

   setoid : Setoid c ℓ
   setoid = record { isEquivalence = isEquivalence }

   open Setoid setoid public using (preorder)


How does it look defining its values via copattern matching? 
What will be its no-eta variant?

Thanks,

------
Sergei