Hola Julián,
Muy interesantes preguntas, paso a responder entre lineas:
Una primera idea es que queremos que la relación R sea funcional para que al menos esa parte del tipado con suertes sea dirigida por la sintaxis, no? (No sé del resto si es dirigido por la sintaxis o no.)
Si, R es funcional, pero no por esa razón (de hecho el sistema de tipos no es syntax-directed por la regla de conversion (la última)). La razón es que cada tripleta te define una única regla de formación de tipo producto dependiente, y esto es deseable desde el punto de vista lógico-matemático. por ejemplo, la tripleta <Set,Prop,Prop> establece que un tipo producto dependiente bien formado sería (x:T)U donde T:Set, U:Prop (indexado probablemente por x, entonces es un predicado en elementos de T) y todo el producto es de tipo Prop. Es decir, toda cuantificación universal sobre elementos de un set y una función proposicional se puede expresar y tipar en este sistema.
Segundo, en R están las 9 = 3^2 parejas posibles de "inputs" entre Set, Prop y Type_i (de nuevo pensándola como función), y en todas se comporta como la segunda proyección. Salvo en la de (Type_i, Type_j, Type_max{i,j}) que toma el máximo.
Me resulta muy poco intuitivo esto. Yo hubiese tomado un máximo en todas por ejemplo.
Para ser totalmente precisos, y actualizados, hay algunas de estas tripletas que ya no valen más en Coq (por ejemplo <Prop,Set,Set>) pero son las originales del Cálculo de Construcciones como lo definió Thiery Coquand en su tesis de Doctorado.
La respuesta a tu segunda observación, responde a tu tercera pregunta también: Set y Prop no están ordenados (no podes definir un máximo). Si, es un orden parcial, donde Set < Type y Prop < Type, que se puede entender como Type0, y luego viene la jerarquía de universos de Tipos (Type0 < Type1 < ...).
Espero haber sido claro y respondido tus dudas.
Saludos,
Gustavo