Why are sForall and sExists defined the way they are?

Stream: iris-lean

[Markus de Medeiros]

Anyone have any clue why sForall and sExists in BIBase are defined like

  sForall : (PROP → Prop) → PROP
  sExists : (PROP → Prop) → PROP

instead of the way it's done in König's thesis as well as Rocq Iris?

  sForall {A} : (A → PROP) → PROP
  sExists {A} : (A → PROP) → PROP

[Mario Carneiro]

The reason for this is because the type of {A} there is hidden and important

[Mario Carneiro]

it's {A : Type u}, and it causes a universe bump in BIBase and also restricts the usage of forall to that particular type universe

[Mario Carneiro]

this is actually a problem in iris as well, it's just more well hidden there because of the use of template universe polymorphism

[Mario Carneiro]

by using sets instead and defining indexed forall in terms of set forall, it's possible to get the best of both worlds: no universe bump and you can index over types in any universe, even larger than the BIBase itself

[Mario Carneiro]

We have analogous difficulties when defining complete lattices in mathlib

[Markus de Medeiros]

Okay, cool. Am I understanding correctly that the "set" in the "set forall" is analogous to image of the function in the "Rocq forall"?

[Mario Carneiro]

yes