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:
For the Metatheory of Type Theory, Internal Sconing Is Enough
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
https://arXiv.org/abs/2302.05190 https://arXiv.org/pdf/2302.05190
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
anda : 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
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