[Agda] Naive person's questions about agda vs. haskell symbol notation

[Peter Hancock]

I have never properly learnt to use Agda's fancy notational features,
except in a basic ad-hoc way, that accomplishes most of what I want.  I'm
not referring to unicode symbols and whatnot, but the business of making
symbols by scattering '_' characters in some line-noise.

I'd like some hints and tips about how to get the most out of this feature.
RTFM with a pointer would be fine.

Away from the keyboard, I often use some haskell-like apparatus for dealing with infix
symbols.  Namely:

* "section notation", as in (*), (*a), (a*), where * is binary infix.
  Anything that avoids having to write a lambda-expression or think 
  of a bound-variable name is great.
* "backtick" notation, as in (a `foo` b), where foo is a name.  Something
  that turns a short name into an infix symbol is great.
* I very much like the notation  (a <| b |> c) for "if b, then a else c"
  that allows three-place relations to masquerade as infix relations. 

How much of this can be supported or emulated with Agda's symbol-wizardry? 

Hank