Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

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

Напомню, что в теории порядков идеалом называется такое подмножество 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, да придать этому смысл в линейных теориях зависимых типов...
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment