I'm going to be really blunt here: if you don't care about trans people, if you even remotely think there's the slightest hint of merit to the blatant genocidal actions that are going on in the US right now, you can fuck right off from my projects, spaces, and communities.

I don't give a fuck about "tech shouldn't be political" garbage takes. Tech is made by people and right-wing legislators in the US are trying to *kill* my colleagues right now. There is no tech without people.

Well, I am not surprised, because set-theoretical models of MLTT with induction-induction require large cardinals (see Peter Dybjer work) and so a naive argument won't work for what you want to establish.

Rewording a bit (mostly for my sake):

- We can define a type family whose fiber at a pattern-qua-term encodes the "possible recursive calls" that can be made in that clause
- For most types this family depends only on the type(s) of the function(s) you want to define, and is totally insensitive to the actual function definition
- For inductive-inductive types, this family additionally depends on (parts of) the function definition(s)
- So we can't use its values to guide a translation into eliminators, since instantiating the family requires you to already have a translation into eliminators

Anyway I'm either missing something really obvious that'll have me feeling dumb in the morning or I just stumbled onto a massive edge case we had all tacitly agreed to handwave away

In defining Below for `Pi Gamma A B`

you could try to quantify over the witness of P (Gamma, A) required to state the type of "the recursive call at B" — but neither of pi or sigma let you state that the recursive call has the right type (with sigma you lose the connection, with pi you get too many recursive calls, one for each proof of P (Gamma, A))

Induction-induction is hard because the usual approach to getting rid of structural recursion — defining a family "Below", using the eliminator(s), which packages together all the possible recursive applications, then proving a boosted up induction principle in terms of that — does not actually work anymore.

For ordinary types, even mutual induction, you can define the family(ies) "Below" in terms purely of the *motives* — approximately standing for "the type of the recursive function you will define". But for induction-induction, that's not enough: you also need some of the *methods*!

Consider the inductive-inductive syntax of types and contexts: contexts can be empty or extended, and types are closed under pi. I've attached a scribbled note with the type and its eliminator.

Anyway, if we try to play out the construction of "Below" for this type, you'll see that in the case of Π, there is a recursive call whose *type* depends on the *method* associated with the context-extension constructor. This also shows up in the eliminator, but there we have the methods anyway.

Anyway, there's a cycle I don't know how to break here:

- You need the Below family to guide the translation from pattern matching and recursion to methods and eliminators
- For induction-induction, the Below family is defined in terms of not only the motives but also the methods corresponding to any constructor used in the indices
- The RHSes corresponding to those methods can also make non-trivial recursive calls

To translate mutual recursion on an inductive-inductive type into eliminators, you must first translate mutual recursion into elimination 😵💫

i WILL find the solution to (higher) (nested) (indexed) (inductive-) inductive (-recursive) types, and recursion on them, or die trying(?)

i read the next two emails and things have cooled back down in the indexed inductive types fandom

I'm looking forward to going around making things opaque. Since I find the latter more intuitive I defined quotients in terms of coequalisers for the 1lab. Normally this is fine but sometimes I'll normalise a goal too far and get shit like "Coeq (\x → x .fst .fst) (\x → x .fst .snd)" which is objectively useless. Very high on the opaque to-do list.

Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).

I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️

Joined Jan 2022