Dlaczego wykresy refleksyjne dla parametryczności?

Patrząc na modele polimorfizmu parametrycznego, jestem ciekawy, dlaczego stosowane są kategorie wykresów refleksyjnych ?

W szczególności dlaczego nie zawierają składu relacyjnego? Patrząc na modele, wszystkie wydają się potwierdzać naturalne pojęcie składu relacyjnego:

Najnowsze artykuły, które używają wykresów refleksyjnych, wydają się przyjmować to za pewnik, a jedyny starszy dokument, jaki mogłem znaleźć, który omawiał to „Relacyjna parametryczność i zmienne lokalne” autorstwa O'Hearn i Tennent, którzy mówią:

Jednym z powodów niewymagania kompozycji jest to, że, jak dobrze wiadomo, kompozycja nie jest zachowywana przez relacje logiczne wyższych typów.

I nie jestem do końca pewien, co to oznacza, więc moje pierwsze pytanie dotyczy tego, co mam na myśli, i mam nadzieję, że będzie to lepsze odniesienie do tego pytania.

Myślę, że to oznacza, że ​​na przykład wykładniczy niekoniecznie zachowuje relacyjną kompozycję na nosie. W szczególności nie możemy pokazać . Oznacza to, że wykładniczy nie rozciąga się na funktor kategorii powiązań.$(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)$

Od miesięcy, kiedy zadałem to pytanie, wydaje mi się, że znalazłem rozsądną odpowiedź.

$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$