Amélia Liao @amy@types.pl

i want a red herring principle poster featuring like.. a blue sardine

woke up too early, decided to sleep some more, missed my alarms entirely

g r e a t

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 😵‍💫

slowly becoming a Sized Types Gal

Does anyone have a pdf of Eduarde Giménez. Codifying guarded definitions with recursive schemes. Types for Proofs and Programs, ’94?

Time to go to campus and repeatedly make up recursive functions to get mad at

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

somewhere in between what the existing literature describes and what agda implements is a sound, expressive approach to termination checking which scales to univalence and impredicativity both

this might be my first proof of ⊥ in stable safe agda 🎉​

spent over an hour trying to come up with a fancy counterexample to a wonky behaviour assuming propositional resizing when the counterexample i discarded as "too obvious" would actually have worked

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

things are heating up in the indexed inductive type 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.

I'm very concerned that I can remember all the built-ins while asleep...