1. Jesper Cockx has a new paper out with students of his at ICFP that involves, presumably, Agda and dependent types
2. I have only ever presented papers at reading group in which he is one of the authors
3. There is one last reading group left before I leave

What if... What if...

I suppose I could skim it over a bit rn to see if it's something I could decently understand well enough in a week

Oh this sounds very cool

I was gonna say NoConfusion looks v handy for the ordinals stuff I was doing, but I just remembered I didn't need it in Agda, only in Coq, since pattern matching takes care of things for me

Wait wait wait. What about inductive–inductives

Me: it's so annoying when reviewers ask about things clearly outside the scope of the paper
Also me: immediately starts asking about things clearly outside the scope of the paper

oh it's not true that I've only presented papers with Cockx on them. I did TTobs I think

Induction–recursion with functions to universe levels?????

I just noticed that universes are basically cumulative with respect to Set omega, like every Set is in Set omega despite then being predicative otherwise
Like. What.

Great now I gotta focus enough to read it through without getting distracted by how much levels look like sizes

I'm spending so much time on telescopes bc this is so confusing lol

Okay this ConDesc thing is on clever. It took me way too long to figure out what it was doing but somehow this is indeed the correct grammar for describing strict positivity
I think it would've been helpful to give a little... diagram? Illustrating how it looks nondependently
Like my notes rn look like

A ::= X (var)
  | S -> X (pi)
  | A -> A (otimes)

where X is the recursive argument and S is an arbitrary type (not incl. X since it's not in scope technically)

The interpretation of datatype descriptions is incredibly confusing omg. What's going on

ω×ω WHAT is this thing. what is it. Agda explain yourself