[Iris-Club] Several small questions on Iris

Robbert Krebbers mail at robbertkrebbers.nl
Thu Feb 16 10:44:42 CET 2017

On 02/16/2017 10:25 AM, Ralf Jung wrote:
> We currently do not have CMRAs of different sizes; doing so would
> require using Coq's universe polymorphism to have a CMRA structure for
> every universe that can contain CMRAs of lower universes.  I guess if we
> did that we could parameterize all our proofs by the universe level that
> is used for the "big product", making all lower universes available for
> the user-supplied CMRAs.  Combining different proofs would use the
> maximum universe.
>   That could work, but (a) it's very different from what you suggested
> [so it doesn't help me understand your question], and (b) messing with
> Coq's universe polymorphism like that sounds very daring and asking for
> trouble. ;)
c.) What we "actually" want is to have a big product over all ofe -> 
cmra functors, i.e. instantiate Iris with the functor:

   F : ofeT -contractive-> cmraT
   F(X) := nat -fin-> { G : ofeT -contractive-> cmraT  &  G X }

And solve:

   iProp ~ uPred (F (▷ iProp))

However, even mathematically speaking (ignoring how to model this using 
universe polymorphism in Coq) this does not make sense: iProp itself 
will be big, hence the cmra in the range of G in the Sigma-type will be 
big, hence F will be bigger, hence universe inconsistency.

More information about the Iris-Club mailing list