Почему рефлексивные графы для параметричности?

Глядя на модели параметрического полиморфизма, мне интересно, почему используются рефлексивные категории графов ?

В частности, почему они не включают реляционную композицию? При взгляде на модели все они, кажется, поддерживают естественное понятие реляционной композиции:

$$x(R;S)z \iff \exists y. xRy \wedge y S z$$

В последних работах, в которых используются рефлексивные графы, кажется, что это само собой разумеющееся, и единственная старая статья, которую я смог найти, которая обсуждала это, была «Реляционная параметрическость и локальные переменные» О'Хирна и Теннента, которые говорят:

Одна из причин, по которой не требуется составляемость, состоит в том, что, как хорошо известно, композиция не сохраняется логическими отношениями на более высоких типах.

И я не совсем уверен, что это значит, поэтому мой первый вопрос заключается в том, что подразумевается под этим, и, надеюсь, лучше справиться с этим вопросом.

Я думаю, это означает, что, например, экспонента не обязательно сохраняет реляционную композицию на носу. В частности, мы не можем показать . Это означает, что экспонента не распространяется на функтор в категории отношений.$(R;R') \to (S;S') \equiv ((R \to S);(R' \to S'))$

$((R \to S);(R' \to S')) \subset ((R;R') \to (S;S'))$

$f((R \to S);(R' \to S')) h$$g$$f(R\to S)g(R'\to S')h$$xRyR'z$$f(x) S g(y) S' h(z)$

Через несколько месяцев после того, как я задал этот вопрос, я думаю, что нашел разумный ответ.

$R : D \to E$$\omega$$\omega$$|D|\times |E|$$R : \omega + 1 \to \mathbb{N}$$\omega+1$$\mathbb{N}$$R(n,n)$$R$$R;R^T : \omega+1 \to \omega + 1$$n R;R^T n$$\omega R; R^T \omega$