July 22nd, 2020

ДР Цертуса 2011

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.