Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

Embracing Largeness and Taming it

What's missing to Intuitionistic Type Theories (ITTs) is the ability to talk about, say, all groups: you can talk only about `U`-small groups for a given universe `U` there. It is not the case in case of Construction Calculi (common generalisation to ITTs and second-order lambda calculus System F).

In a particular Construction Calculus variant we're developing (Cedille Core with Reflective Univalent Universes), it is possible to define the type classes like `Group[T : *] : *` supplying a group structure on the type `T`. In general, carrier is not limited to be a single type, it can be a pair of types, a type former (say, `Endofunctor[F : * -> *] : *`), a sequence of types (say, `Spectrum[Ts : Nat -> T] : *`) or even something dependent, say `Category[Ob : *, Hom : Ob -> Ob -> *] : *` that supplies a type with a and a type and a type twice indexed by the first type by the structure of a category.

You can actually provide proofs and constructions for _all_ groups, say `DirectProduct[A B : *](G : Group[A], H : Group[B]) : Group[A × B]`. Functors between categories and natural transformations between functors are definable too: their carriers are complicated, but feasible to work with.

Furthermore, there you actually do have a notion of locally-small category of structured objects. It takes a typeclass on * (like Grp) as the first parameter:
LSCategory[Str : * -> *, Hom : (X Y : *) -> Str[X] -> Str[Y] -> *]

Even more generally, for any theory T presented in intuitionistic first order logic with dependent sorts (FOLDS) one can define a respective locally-small n-category of models. Any theory `T` has a fixed dependency depth `n` and fixed carrier kind `ϰ` the definition of respective n-Categories starts like
LSᵀCategory[Str : ϰ -> *, Hom : (X Y : ϰ) -> Str[X] -> Str[Y] -> *, Hom₂ : ···, Homₙ : ···]`.

In particular, one can define a locally-small 2-category of small categories and so on, with their respective functors, natural transformations etc.

It is not possible to abstract on kinds `ϰ` and thus also theories `T`, but it seems undesirable. We strive to develop a calculus with strong reflection properties (large objects behave exactly like `U`-small ones), so that we can derive a metatheoretical result that one can actually always work with U-small ᵀCategories, on which level abstracting on `T` is surely possible.

  • Towards Univalent Construction Calculus

    Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning. By “modern”…

  • (no subject)

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

  • Прогресс

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

  • Post a new comment


    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.