Show newer

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

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
Show thread

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

Show thread

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))

Show thread

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

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(?)

Show thread

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 🎉​

Show thread

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

Show thread

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.

sometimes i do wish i had gone into one of the sciences instead of maths/computer touching. not from any serious displeasure but (and this is my chuunibyou-est opinion) because i think lab coats are rad. if given the opportunity i would dress exactly like makise kurisu.

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

Show thread
Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.