AndrasKovacs @AndrasKovacs@types.pl

Any language that allows name shadowing should support positional/De Bruijn variable notation too.

This occurred to me yesterday while working on my cubical TT, but in retrospective it's pretty obvious.

In any local scope, the output of user interaction should be well-formed in that scope, and there should be a way to print any output in a re-checkable form. Shadowed variables from local scope can easily occur in interaction output, so the language must support a way to refer to them.

I wrote a big Proof Assistants answer on induction features in Agda.

In short, the main features which are not in any literature, to my knowledge, are:

• Most nested induction features.
• Many induction-recursion-like patterns, including "double induction-recursion", which is useful for defining setoid universes.
• Recursion-recursion.

Correction/addendum: type is only a full Palmgren-style super universe if we have large elimination from all type formers to it. Usually that's not the case in type theories; for example we can't compute a proper type from Nat because it would require abstracting over a type.

So the HoTT-intro definition isn't as strong as a super universe, but it does have a super-universe-style alternate specification. In this weaker version we get next universes, joins, and universes containing each type from a finite list, but we don't get transfinite hierarchies.

Some comments on the specification of universes in "Introduction to HoTT" chapter 6: https://arxiv.org/pdf/2212.11082.pdf The idea is that instead of working with some concrete level-indexed hierarchy, we assume to have "enough" universes. I've seen some positive reception to this.

First, it seems to me that the "enough universes" rule is equivalent to Palmgren's specification of super universes: http://www2.math.uu.se/~palmgren/universe.pdf

As a short summary, if types in some type theory form a super universe, that means that for each type family there is a universe which contains it.

In other words, given A type and
a : A ⊢ B a type, there is a U A B type and c : U A B ⊢ El A B c type which is closed under usual assumed type formers, and additionally A is contained in U A B and for all a, B a is contained in U A B.

This operation immediately gets us a "next universe" for each universe. We can also take a "join" of universes by taking the U of a coproduct of types of type codes.

I find the book definition (6.2.1) somewhat awkward in comparison. As I see, the intention of the definition is to allow arbitrary telescopes as input (not just a single type family), containing any number of type families of different arities. But

• The definition doesn't use actual telescopes, but instead allows a context of dependencies to be specified for each type. So this is a rule which is non-uniform in contexts, so we can't write it in a second order (or higher-order) signature.
• Universes with telescope inputs can be derived from Palmgren's rule by iterating universe joins and universe formation. Super universes are also easy to specify in second order signatures.
• In any case, we don't need telescopic inputs to concisely define the next universe operation, the join operation, and to grab a new universe which contains each type from a list.

On a different note, I'm not really convinced that super universes (using any specification) are good to have in introductory material. I'm in a reading group of the book, which has several beginners, and I looked more closely at this chapter because one participant was confused by it.

Vanilla Nat-indexed universes seem like the best choice to me. In any case it is required that informal exposition can be in principle elaborated to formal syntax. I'd rather tell students to find a consistent Nat-level assignment ("typical ambiguity" style) than to appeal to a more complicated high-powered rule.

I wrote a bit about higher induction-induction-recursion: https://gist.github.com/AndrasKovacs/16ce01ad516b3f757ff5d88276f1c515 Maybe I'll develop this more in the future.

These slides from a talk about my thesis might be interesting as well: https://andraskovacs.github.io/pdfs/wg6stockholm.pdf

First post here. I defended my thesis last Friday. You might want to check it out: https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf