mutual inductive definition

Stream: new members

[Shaun Steenkamp]

can one of you explain why I cannot get this mutual inductive definition to work?

mutual inductive Foo, Bar
with Foo : Type
| bizz : Foo
| buzz {f : Foo} : Bar f → Foo
with Bar : Foo → Type
| baz (f : Foo) : Bar f

For reference, the following works in Agda

mutual
  data Foo : Set where
    bizz : Foo
    buzz : {f : Foo} → Bar f → Foo

  data Bar : Foo → Set where
    baz : (f : Foo) → Bar f

[Mario Carneiro]

this is called an inductive-recursive definition, and it is stronger than lean's axiomatics

[Mario Carneiro]

There may be another way to encode the type you want, but inductive recursive definitions can be used to prove DTT is consistent, so lean can't do it

[Keeley Hoek]

Incidentally, Mario, were you working on a Lean consistency project at some point?

[Shaun Steenkamp]

What is DTT?

[Patrick Massot]

dependent type theory

[Patrick Massot]

That's the name of the game we are playing

[Mario Carneiro]

yes, I'll be defending my masters thesis in a few weeks and lean consistency is in it

[Mario Carneiro]

https://github.com/digama0/lean-type-theory/releases/tag/v0.21

[Kenny Lau]

so, is lean consistent?

[Abhimanyu Pallavi Sudhir]

@Kenny Lau How is that not independent?

[Mario Carneiro]

yes, assuming some large cardinal assumptions

[Mario Carneiro]

which is the usual story with consistency proofs

[Johannes Hölzl]

I think this shape is called inductive-inductive: mutual inductive types where at least one is indexed by the other one, inductive-recursive means to mutually define inductive types and recursive definitions where at least one inductive type depends on the recursive definition.
I think inductive-inductive can be reduced to inductive, inductive-recursive cannot

[Mario Carneiro]

you might be right about the name, but I'm pretty sure inductive-inductive is also axiomatically strong

[Mario Carneiro]

because you can define the well typed terms of DTT by induction-induction with the set of well formed contexts and the set of types in a context

[Mario Carneiro]

Inductive recursive can be reduced to inductive inductive, I think, where the recursive function becomes a functional relation

[Johannes Hölzl]

Ah, or it was this way round

[Shaun Steenkamp]

There may be another way to encode the type you want, but inductive recursive definitions can be used to prove DTT is consistent, so lean can't do it

Consistent with respect to what?

[Johannes Hölzl]

with respect to DTT with a larger type universe and inductive recursive definitions (I guess)

[Floris van Doorn]

This is indeed an inductive-inductive definition. I think adding these won't increase the proof stength of the system. In extensional type theory, inductive-inductive definitions can be defined from indexed inductive types, but I don't think it's known in whether this is the case in intensional type theory.
Inductive-recursive definitions indeed do increase the proof stength of the system: you can build a (Tarski) universe using induction-recursion.
Ncatlab links:
https://ncatlab.org/nlab/show/inductive-inductive+type
https://ncatlab.org/nlab/show/inductive-recursive+type