There are three parameters in _∷⟪_⟫_
which are the underscores.
Number them _1 ∷ ⟪ _2 ⟫ _3
for convenience below:
The type (x : ℕ) -> min ≤ x -> MinList x -> MinList min
has 3 parameters and the result type.
_1 : (x : ℕ)
_2 : min ≤ x
_3 : MinList x
The << and >> unicode are just names, nothing special. See
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Names
and
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Mixfix