Вселенные, идеалы и классы

Напомню, что в теории порядков идеалом называется такое подмножество I предпорядка (O, ≤), что
(а) для любых a b : I найдётся с : I, такой что с ≤ a и с ≤ b,
(b) для любого x : I всякий y ≤ x тоже в I.

Про теорию типов O с сабтайпингом ≤ говорят, что она снабжена иерархией кумулятивных a la Russel вселенных, если задано семейство типов U_i : O, такое, что для каждого T : O найдётся такой U_i, что T : U_i, и семейство U_i образует идеал.

Теории множеств, такие как NBG, оперируют двумя типами сущностей — собственно множествами и классами, среди которых есть proper classes, и классы, представимые множествами. Как известно, если рассмотреть топос, порождённый теорией множеств, то классы играют роль идеалов этого топоса. Представимые множествами классы — это главные идеалы (т.е. порождённые одним элементом), а вот остальные идеалы — proper classes.

Как бы понять, в каком смысле класс Set аналогом идеала расселовских вселенных?..

Как бы понять полиморфную по вселенным квантификацию (∀x : Type) T как class bound quantification, т.е. не как псевдокод, и не как не морфизм из конкретной вселенной U куда-то ещё, а морфизм на уровне идеалов, и как-то увязать это с параметрическим полиморфизмом, как-то увидеть, что если мы не для конкретного типа T, а для всего класса Type имеем id : (∀x : Type) X -> X или NNO : (∀x : Type) (base : X, step : X -> X) -> X, то эти штуки пропозиционально равны функции id и типу Nat соответственно. А в идеале позволить и для главных идеалов порождённых типом X осуществлять номинальную квантификацию (∀x : X) Y, являющуюся ослабленной формой обычного пи-типа (x : T) -> Y, да придать этому смысл в линейных теориях зависимых типов...