Polymorphic universes in Coq are complicated
Together with cumulativity, inductive types have variance information on them inferred from subtyping the constructors at different levels

The universe level constraint collection system seems very inherent to the core type system
Like it's not like it "really" elaborates to some more explicit version (which makes sense, since that would need to solve the constraints)

Baffled I am

No it makes sense
I've seen the inside of the kernel before, I know that it proceeds structurally first so it would check that h ~ h and then (fun x => f x) ~ f and then it checks eta

Coq's convertibility relation is implicitly congruent in a way that the manual doesn't mention, probably because it is so obvious that it should be that way that it just doesn't say

This does mean that both reduction and equivalence need to have a bunch of compatibility rules, but in Coq "reduction" as in running a program is entirely separate from how it checks equivalence anyway, the former being either CBV or CBN and the latter being a mutually recursive process of reducing to WHNF then congruent equivalence checking then further WHNFing

I certainly can't remove compatibility rules from my reduction since that will preclude CBV essentially, which means I do need them in both
ew

I wrote them in substitution form instead of explicitly for each form for reduction in my rules and surprisingly it works for my proofs
It's just not very algorithmic if you're implementing it
I mean it's pretty much the same structure as the definition of substitution (which... I haven't written out in full either) so it's obvious enough that they're the same

Mathematics is about being convincing, not precise, anyway

That's a hamartia (hamartium?) of proof assistants
Either such precision is required that it obscures the spirit of the argument by showing the trees instead of the forest, or you have tactics that solve everything for you to the point that nothing is convincing

Proof by iauto is basically the mathematician's "Trivial."

Would it be convincing enough to interpret my "inductive" as fixpoints of functors

nvm that OPLSS lecture didn't cover universe levels or Prop. I have no idea how they would work

It's not too important to me whether my source has congruence so my final boss battle is with universe polymorphism

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