doc: expand the <: doc string

Clear up some things, state some expected properties and limitations,
add cross-references, add an academic reference, add more examples.

Author: nsajko

base/operators.jl

@@ -3,10 +3,27 @@
 ## types ##
 
 """
-    <:(T1, T2)
+```julia
+<:(L, R)
+```
+
+The subtyping predicate: test whether the type `L` may be a subtype of `R`.
+
+For any type `A` and any type `B`, `A` subtypes `B` if and only if any value
+belonging to `A` is also of type `B`. Subtyping is reflexive and transitive,
+making it a *preorder*.
+
+Julia is sometimes not able to prove a subtyping relation between two types, even
+if such a relation holds. In such a case the result of `S <: T` will be `false`
+even if `S` subtypes `T`. Even so, `<:` is expected to be reflexive and transitive.
+
+See also: [the Manual page on types](@ref man-types), [`Union{}`](@ref),
+[`Any`](@ref), [`isa`](@ref).
 
-Subtype operator: returns `true` if and only if all values of type `T1` are
-also of type `T2`.
+Julia's subtyping relation is the topic of the paper *Julia Subtyping: A Rational
+Reconstruction*, published in the *Proceedings of the ACM on Programming
+Languages*. DOI: [`10.1145/3276483`](https://dx.doi.org/10.1145/3276483), HAL:
+[`hal-01882137`](https://inria.hal.science/hal-01882137).
 
 # Examples
 ```jldoctest
@@ -16,9 +33,19 @@ true
 julia> Vector{Int} <: AbstractArray
 true
 
-julia> Matrix{Float64} <: Matrix{AbstractFloat}
+julia> Matrix{Float64} <: Matrix{AbstractFloat}  # Invariance
 false
+
+julia> Union{} <: Int  # The bottom type, `Union{}`, subtypes each type.
+true
+
+julia> Union{} <: Float32 <: AbstractFloat <: Real <: Number <: Any  # Chaining
+true
 ```
+
+The `<:` syntax may also be used in another sense; for specifying the lower and
+upper bound on a parameter of a [`UnionAll`](@ref) type, see the Manual section on
+[UnionAll types](@ref "UnionAll Types").
 """
 (<:)