[Agda] strictness place

[Sergei Meshveliani]

Dear Agda developers,

can you, please explain, what is the relation between laziness and
strictness in Agda?

Which is the default? Which is favorite? 
Have they equal rights? 

Where strictness can appear? Does the type checker process strictness?
Does the compiler process strictness?

Is Agda ready to take the option "do everything strict in type checking
and in the executable code" ? what will be a real effect?

(As I recall, Haskell needs to define `strict' separately for each
particular constructor or function application, so that `lazy' and
`strict' have not equal rights).

Is it true that Agda only transmits strictness annotations to the
Haskell code, and then GHC processes these annotation according to the
Haskell rules?

So far, I am not going to use strictness explicitly. 
But sometimes I say "Agda has lazy evaluation", and some people object
as "no, it also has a strict back-end ...".
So that I need to have an idea.
Probably, it needs to be "Agda has lazy evaluation as default and
favorite" (?)

Thanks,

------
Sergei