Support for universe polymorphism

[jonsterling]

It would be game-changing to support universe polymorphism. Right now I have a class of large categories, and this is enough for me at the moment, but I would be able to do things so much nicer if I could also speak of small categories without duplicating everything. I realize this is probably quite complex engineering-wise.

[gares]

in progress... @ecranceMERCE is helping, we will get there. tracker:
LPCIC/coq-elpi#315

[damien-pous]

Any news on this front?

HB.mixin breaks syntactically if I "Set Universe Polymorphism", and it says "Attribute universes.polymorphic is not supported" if I start the declaration with "#[universes(polymorphic=yes)]".

[gares]

Well, we started but it far from being done.
I suggest you Unset universe checking in the meanwhile.

[CohenCyril]

Waiting on rocq-prover/rocq#19537

[spitters]

Looks like this has moved to:
rocq-prover/rocq#20574

This issue is also very relevant for us in SSProve.

[spitters]

@CohenCyril when rocq-prover/rocq#20574 is merged will this solve the issues, or will that just be the start of a major operation on the HB side?

[CohenCyril]

There will be a slight adaptation of HB to do, but I don't expect it to be hard.

[spitters]

Thanks @CohenCyril ! Matthieu writes in rocq-prover/rocq#20574
that he's making it available for others to experiment on. Would it make sense to prepare an adoption of HB for it on a branch?

[CohenCyril]

Definitely. I intended to do it at some point, maybe at the rocq 'n'share next month. But I wouldn't mind if someone else tried first.

[spitters]

There's now a paper with an active implementation effort:
https: //github.com/mattam82/coq/tree/universes-clauses
https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper21.pdf

[spitters]

This paper on cat th also requests univpoly for HB:
https://arxiv.org/pdf/2509.17392