[Agda] HO logic

[Sergei Meshveliani]

Can people, please, explain
(in simple words):

what is a high-order logic?

Consider the example of a program in Agda:

--------------------------------------------------------------
open import Relation.Binary using (Transitive; DecTotalOrder)
open import Data.Nat as Nat using (ℕ; _≤_)

open DecTotalOrder Nat.decTotalOrder using () renaming (trans to ≤trans)

Sequence = ℕ → ℕ

_≤s_ : Sequence → Sequence → Set _
f ≤s g =  ∀ n → f n ≤ g n

≤s-trans : Transitive _≤s_
≤s-trans {f} {g} {h} f≤g g≤h n =  ≤trans (f≤g n) (g≤h n)
-------------------------------------------------------------


≤s-trans  is a proof for a formula that ranges over all infinite
sequences over ℕ.  It proves that the relation _≤s_ on these sequences
is transitive.

As Agda type-checks this proof, does this mean that Agda supports an
high-order logic?

Are there some more advanced requirements necessary for high-order
logic?

Thanks,

------
Sergei