Induction-Recursion or Universe ala Tarski?

Stream: Is there code for X?

[Joey Eremondi]

Has anyone been able to get a version of Induction-Recursion going in Lean, or some other way of implementing a Universe ala Tarski?

For those who don't know Induction Recursion is where you define an inductive type mutually with a function that pattern matches on that type. It's useful when you have, for example, a type of codes representing some collection of dependent types, where to encode dependent functions you need to parameterize the codomain over the decoding of the domain.

I've heard folklore than you can fake IR by using impredicativity, but I don't know how that would actually work. I realize it won't be directly supported by Lean but I'm wondering if you can fake it.

[Mario Carneiro]

induction-recursion is axiomatically stronger than lean, so no you can't do it in general. Several specific kinds of inductive-recursive types can be encoded though

[Mario Carneiro]

For Tarski universes things are a little better: Universes like Type u are Tarski universes, so every type is an element of a Tarski universe

[Mario Carneiro]

I guess I should say that you can't do inductive-recursive types without a universe bump

[Wojciech Nawrocki]

Mario Carneiro said:

For Tarski universes things are a little better: Universes like Type u are Tarski universes, so every type is an element of a Tarski universe

I think Lean uses Russell-style universes. Tarski universes would be A : Type u ⊢ El(A) type u.

[Mario Carneiro]

I mean a tarski universe in the set theoretic sense, which is more or less equivalent in strength to a Grothendieck universe which Type u definitely is

[Mario Carneiro]

But it's possible I misunderstood what @Joey Eremondi meant by "Universe a la Tarski"

[Joey Eremondi]

@Mario Carneiro What I meant was a type-theoretic universe where there's a separate type of codes, and an explicit decoding function El : Code -> Type that interprets codes to their types of elements. @Wojciech Nawrocki is right that Lean has a Universe ala Russel, i.e. you can use types on both the left and right of : without having to explicitly decode.

That said, you're not wrong, one large inaccessible cardinal (i.e. a Grothendieck Universe) is enough to give a model of induction recursion, which is enough to define a Universe ala Tarski.