Andrea Vezzosi said Cubical Agda made cubical subtyping coercion-based (
outS) because it's a bad idea to introduce more subtyping relations which complicates the system. Also Agda did not have cumulative universes (it is added now).
So does Agda support any subtyping relations? Without using rewriting and cumulativity options of course.