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.