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.

For the Metatheory of Type Theory, Internal Sconing Is Enough

Rafaël Bocquet, Ambrus Kaposi, Christian Sattler

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.

Show thread

Some comments on the specification of universes in "Introduction to HoTT" chapter 6: 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:

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.

My introduction to homotopy type theory book is finished!

I'm sending it to the publisher tonight, and I'll also upload it to the arxiv.

I wrote a bit about higher induction-induction-recursion: Maybe I'll develop this more in the future.

First post here. I defended my thesis last Friday. You might want to check it out:

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.