Is induction-recursion and induction-induction limitation?

Stream: new members

[Chris M]

The lean prover manual says "In the type theory literature, there are further generalizations of inductive definitions, for example, the principles of induction-recursion and induction-induction. These are not supported by Lean." I read a bit about induction-recursion (wikipedia). This is just a curiosity: Is this something that would ever be useful in formalizing math?

[Mario Carneiro]

You see it used mostly by the type theory fanatics that already see inductive types as a hammer and everything as a nail

[Mario Carneiro]

An example is that you can use an inductive-recursive type to very naturally capture the type of well typed terms mutual with the type of contexts, and so prove the consistency of DTT

[Mario Carneiro]

I forget all the details, but it's something like this:

mutual inductive context, type, term
with context : Type
| nil : context
| cons (Γ : context) (A : type Γ) : context
with type : context → Type
| univ {Γ} : type Γ
| pi {Γ} (A : type Γ) (B : type (context.cons Γ A)) : type Γ
| T {Γ} : term Γ type.univ → type Γ
with term : context → type → Type
| var {Γ A} : term (context.cons Γ A) A
| lift {Γ A B} : term Γ B → term (context.cons Γ A) B
| lam {Γ A B} : term (context.cons Γ A) B → term Γ (type.pi A B)

[Mario Carneiro]

I recall a talk by Peter LeFanu Lumsdaine (I think) about how to represent buildings (some homotopy theory thing like CW complexes) using inductive-recursive types

[Mario Carneiro]

Misremembered the author, but the slides here look familiar

[Kevin Buzzard]

@Bhavik Mehta and I had an interesting discussion about this on the discord a few weeks back. The question came up about higher inductive types and whether they were useful for mathematics, and I said "well I formalised perfectoid spaces and schemes and I didn't need anything apart from structures so clearly they're not important" and then Bhavik linked to a parody article about someone who knows a programming language which is not too high-level and not too low-level and then looks at what the lower-level programming languages do and says "golly I'm glad my language has got these features so you don't have to struggle like they do" and then he looks at what higher-level programming languages are doing and says "they're using all these crazy features and I don't understand their code but it's clearly not necessary because I can do everything I want to do in my language"

[Kevin Buzzard]

the point being that perhaps higher inductive types are useful even though I don't need them

[Kevin Buzzard]

Bhavik will I'm sure remember the link to the parody

[Kyle Miller]

That's known as the blub paradox. Maybe it was Paul Graham's essay that introduced them?

[Kyle Miller]

I guess you said a parody, so probably not. But here's his essay: http://paulgraham.com/avg.html

[Mario Carneiro]

someone needs to write a language called blub

[Kevin Buzzard]

Yeah this is it, perhaps it was someone else's take on Blub but I think it was called Blub

[Kevin Buzzard]

in fact I can now search for it on the discord

[Kevin Buzzard]

oh except I am live streaming at 10

[Reid Barton]

regarding higher inductive types, Lean doesn't have "higher types" in the first place, but you probably used quotients, which you can see as a particular hard-coded baby higher inductive type.

[Reid Barton]

About induction-recursion, I would say: yes, there are definitions in math that can naturally be viewed as examples of induction-recursion; but they aren't of this "model of type theory" sort, and (usually?) can be encoded in other ways. So for the purposes of math, not supporting induction-recursion is sort of like (hypothetically) not supporting mutual inductive types.

[Reid Barton]

Whether it would be useful to have direct support for induction-recursion is hard to say, given that it's not so easy to try using them.

[Bhavik Mehta]

Kyle Miller said:

I guess you said a parody, so probably not. But here's his essay: http://paulgraham.com/avg.html

Yeah this was exactly what I'd linked

[Scott Morrison]

I remember trying to formalise some definition of Jamie Vicary's about higher categories at some point, and realised I was trying to write something than needed induction-recursion. I can't find this now.

[Scott Morrison]

A student at some point claimed that they wanted to use induction-recursion to formalise CW complexes, but I never got to the bottom of their difficulty. I'm pretty confident in that case it was not necessary.

[Devon Tuma]

They may have been trying to do a HoTT style of cell complex, where the type associated to most cell complexes will be a higher inductive type? (e.g. the CW complex for a circle would translate to a type with two constructors: A base point, and a non-trivial path from the base point to itself, a torus would be a type with 4 constructors, etc.) Although this is more a way to look at particular complexes than a generic formalization of them.

[Reid Barton]

If you want to build the type "CW complexes of dimension at most n" as an inductive family indexed on n, then you need induction-recursion in order to say what it means to give attaching maps for the n-cells. But you can also define that type by recursion on n, and this would be supported by Lean.

[Reid Barton]

When I realized this (and that it would also solve another problem of mine) I stopped accumulating a list of examples of induction-recursion in math. :upside_down:

[Reid Barton]

The CW complex example is a bit flawed in that it's not clear how you would describe infinite-dimensional ones.