[Agda] beginner questions

[Serge D. Mechveliani]

People,
I have the following beginner questions.

(1) The example program
            Agda-2.3.0.1/examples/instance-arguments/06-listEquality.agda
ends with 

  test = eq (true :: false :: true :: []) (true :: false :: [])
    where listBoolEq = listEq eqBool

And I do not understand these two lines.
Should it be 
  test = (listEq eqBool).eq 
                   (true :: false :: true :: []) (true :: false :: [])
?

(2) Do there exist papers (manustripts, descriptions, explanation) about 
    the Standard Library (somewhat its principles, architecture etc.) ?

(3) tutorial.pdf  for Agda often writes  T : Set,
    while Standard Library writes        T : Set a,
where I expect `a' to be a type parameter. So, `small' types look like
being parameterized by a type `a'.
Some small comment is nedeed.
Does this mean that  T  is any `small' subtype in a type `a' ?

(4) Instances in the Standard Library.
The Standard Library lib-0.6 provides the `classes' (records) for
Semigroup, Group, ..., Ring. 
Does it also provide some classical instances for them?
For example,
* the instances up to  CommutativeRing  for  Integer
  (CommutativeSemigroup, CommutativeGroup  for  +,
   CommutativeSemigroup, CommutativeMonoid for  *,
   distributivity, CommutativeRing
  ),

* the instance (record map)
  (Ring A, Ring B) => Ring (A, B) where  -- coordinatewise operations
                                         -- in the direct product A x B
How could these instances (record maps) look?


(5) On the practice of dependent type programming
    (sorry for a naive question!).

tutorial.pdf  for Agda writes in  Chapter 2.5 "Programs as proofs"

  lookup : {A : Set}(xs : List A)(n : Nat) ->
                                      isTrue (n < length xs) -> A
  lookup []        n       ()
  lookup (x :: xs) zero    p  = x
  lookup (x :: xs) (suc n) p  = lookup xs n p

What is its expected usage on practice? 
For, example, "the 20-th element in the charater list  ['a' .. 'z']" 
(the segment from 'a' to 'z')" :

  lookup ['a' .. 'z'] 19' p    -- 19' abbreviates 19 in the unary system.

What does one need to put for  p 
(of the type  isTrue (19' < length ['a' .. 'z']) 
?
Must it be any `proof' of the statement  (19' < length ['a' .. 'z'])  ?
And where does one take such a proof? Has one to write

  lookup ['a' .. 'z'] 19' p   where
                              p = if 19' < length ['a' .. 'z'] then
                                                         trivial : True 
                                  else  ()  -- ?
?

Thank you in advance for explanation,

------
Sergei
mechvel at botik.ru