I'll talk about this declaration only:

data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where
PrO : {lte : a -> a -> Type} -- <=
-> ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z)
-- transitivity
-> PreOrder a lte

This declares a function `PreOrder`, which when given some type called `a`, and some function from two `a`s to some other type, produces a type itself. The reason why we see `(a : Type)` to give a name to `a` is that the name is re-used in the second argument.

To produce a value, a constructor is defined `PrO`, with one _implicit_ argument `lte` of type `a -> a -> Type` (note that this `a` is not the same `a` in the type for `PreOrder`!) that can be inferred from the other arguments, and one other argument of a complex type we'll dig into in a moment. If you supply `PrO` with these two things, you will get back an inhabitant of type `PreOrder a lte` - the type that `PreOrder` promises to return when given two things. This is the same as `Maybe` in Haskell being a type-level function, and `Maybe Int` being a type, where `Just` is a constructor that can produce a `Maybe Int` given an `Int`, and `Nothing` is a constructor that can also produce a `Maybe Int` out of nowhere.

((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z)

This type is interesting because of the Curry-Howard correspondence, which basically says that types and propositions are the same thing, and expressions and proofs are the same thing. If you can show there exists some value of some type, you have proven the proposition the type represents. If you think about what `foo :: Int -> String` means in Haskell, you could turn it around to say "If there is an Int, then there is a String." Given some "proof" that `Int` is a non-empty type, that is, a value of type `Int`, can you prove that there exists some value of type `String`? Well, of course you can: `foo _ = "const"` is one such proof, as is `foo = show` or `foo x = if x < 10 then "less" else "greater"`.

In Idris, we can express much more interesting types, such that the existence of some expression of that type is non-trivial. The above type signature is best viewed IMO as a predicate:

∀x, y, z ∈ a. x ≤ y ∧ y ≤ z ⇒ x ≤ z

Remember that `a ⇒ b ⇒ c` is the same as `a ∧ b ⇒ c`, just curried, the type signature above is saying that given any x, y, z of type a, and some value indicating that `lte x y` is "true", and some value indicating that `lte y z` is "true", it can be shown that `lte x z` is "true" too. That is, a value of that type is a proof that `lte` is transitive.

Given some _user supplied_ proof of transitivity, and the implicit transitive operator, we have an inhabitant of the type `PreOrder a lte`.

This is dependently typed, because the _type_ of `lte x y` depends on the _value_ of `x` and `y`. When we say `lte : a -> a -> Type` we mean that `lte` is a function from two values of type `a` to some other type.

As an example, we could write `badlte : Int -> Int -> Type; badlte _ _ = Int`. This comparison operator simply ignores its arguments and says the Type of all such comparisons is always `Int`, which is the same as saying that all `Int`s are equivalent, because the binary relation is inhabited for every possible pair of `Int`s. We can prove transitivity with the lambda expression `\x,y,z,ltexy,lteyz => 42`, that is, given three values and two proofs that x <= y and y <= z, we can "prove" x <= z because we can show there's an inhabitant for the type of `Int`. We can make a preorder, and a totalorder, and sort using this order (the result is that any permutation of the input list is fine, because everything's equivalent for comparison).

As a more _interesting_ example, consider the definition of `LTE` for the type `Nat`:

data LTE : (n, m : Nat) -> Type where
LTEZero : LTE Z right
LTESucc : LTE left right -> LTE (S left) (S right)

This is an inductive type definition that depends on the values given. `Z`, or zero, the base case of a `Nat`, is less than or equal to every other value, so we can use `right` as a placeholder variable. Given the proof that `left <= right`, we can also say that the successor of `left` (`S left`) is less than the successor of `right`. This is a bog standard inductive proof form, transposed to code. `LTE` becomes a function from two `Nat`s to a `Type` - but it's a partial function, or relation, because not every `Nat` pair produces a `Type`. If we want to prove that 2 is less than or equal to 3, that is, `LTE 2 3`, we can construct it inductively: `LTESucc (LTESucc LTEZero)`, that is, given `0 <= 1` we can show `1 <= 2` and from that `2 <= 3`. But there's no way to chain `LTESucc` and `LTEZero` together to wind up with `LTE 3 2`.