Formal description of algorithmic subtyping/cumulativity

Question

Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the manual's description doesn't seem to be complete (e.g. you wouldn't be able to derive (λ_: Prop. Set) True ≤ (λ_: Prop. Type) True from what it lists alone), and refers to transitivity, which as a rule wouldn't be algorithmic anyway, I don't think. The only other proof assistant I know with cumulativity is Arend, but their docs don't detail rules either. (Are there more?)

I've seen formal descriptions of subtyping and their derivation rules in papers like pCuIC and the ones it cites, but they all seem to include some form of a transitivity rule (either A ≼ B ≼ C or A ≈ B ≼ C ≈ D). I'm particularly interested in an algorithmic presentation that's known to be sound wrt these usual presentations of subtyping with a transitivity rule.

Answer 1

For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ones around are starting to be quite behind the formalization, hopefully there will be a new one soon).

Answer 2

See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.