Define [tele_arg] as a fixpoint

The current definition of tele_arg increases the universe level in a way that is unfortunate. In particular,

Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...

In Iris, what this means is that bi_tforall/bi_texist have different universe levels than bi_forall/bi_exist. This MR re-defines tele_arg as a fixpoint, which prevents the universe bump. In particular:

Fixpoint tele_arg (t : tele@{u}) : Type@{u} :=
  ...

With this definition, the universes for the telescopic quantifiers can match the universes of the non-telescopic quantifiers in iris (this enables a separate MR to iris: iris!781 (merged)).

mentioned in merge request iris!781 (merged)

changed the description

added 8 commits

• b7f8e49a...56558ffb - 5 commits from branch iris:master
• 5d70db7d - Defining [tele_arg] as a [Fixpoint] avoids a universe bump.
• 31424ff8 - Make [tele] cumulative universe polymorphic.
• f690f54f - Add a universe polymorphic [sigT].

Compare with previous version

resolved all threads

added 1 commit

• 85126794 - Compatibility with Coq 8.11 (by @Blaisorblade)

Compare with previous version

I don't understand universes well, so I find it hard to understand this MR.

Could you do the following to help me:

• Explain why we need Unset Universe Minimization ToSet
• Explain why we need Local Set Primitive Projections, that seems orthogonal?
• Explain why tele needs to be Cumulative and why tS does not need to be.
• Include some test cases so that we can see what did not work before and what is enabled by the MR.

• Unset Universe Minimization ToSet -- nothing in this file should be about Set, but I'm fine dropping it.
• Set Primitive Projections -- these yield better term representation for projections from records. Namely, the parameters of the record are not repeated when the projection is used. I'm fine if you want to remove it.
• I think it is fine to make tS Cumulative. It is probably the right thing to do.
• iris!781 (diffs) that line is not possible without this MR.

@robbertkrebbers @jung Thanks for the feedback so far. I am mostly interested in your thoughts on the universe questions in iris. We've run into some places where universes haveprevented us from using bi_tforall and bi_texist and I believe that the change in Iris (other MR) would address these issues.

My thoughts are that I don't know anything about universes so if you say this improves the situation then I trust you on that. :)

You say you believe that this change helps; could you verify that? Ideally we would have a small testcase in the Iris test suite that uses bi_tforall and currently breaks, and is fixed by your MRs.

added 1 commit

• c74e4be0 - Fixup from the review.

Compare with previous version

added 1 commit

• 6e699f67 - Adding a test file.

Compare with previous version

added 1 commit

• cd53abd2 - Make [tele_arg_cons] cumulative.

Compare with previous version

@jung @robbertkrebbers What are the next steps for this?