How do the universe levels work?

[Deleted user]

I'm trying to start a proof of Beck-Chevalley conditions for adjoint pairs in the yoga example. This involves composing functors, so I started by trying the following just to see what would happen:

Operator cmp : (0;0).

[cmp(g;f)] =def= [lam(x. g (f x))].

Theorem Cmp : [
  {A:U{i}} {B:U{i}} {C:U{i}} {D:U{i}}
  {f : B -> A} {g : C -> A} {k : D -> B} {h : D -> C}
  {p : =(cmp(UpperStar(D;B;k); UpperStar(B;A;f));
         cmp(UpperStar(D;C;h); UpperStar(C;A;g));
         (Psh(A) -> Psh(D)))}
  unit
] {
  unfold <cmp UpperStar UpperShriek Psh>; autoR.
}.

This fails with the following:

Remaining subgoals:

1. [A] : U{i}
2. [B] : U{i}
3. [C] : U{i}
4. [D] : U{i}
5. [f] : B -> A
6. [g] : C -> A
7. [k] : D -> B
8. [h] : D -> C
9. _ : A
⊢ =(U{i}; U{i}; U{i})


1. [A] : U{i}
2. [B] : U{i}
3. [C] : U{i}
4. [D] : U{i}
5. [f] : B -> A
6. [g] : C -> A
7. [k] : D -> B
8. [h] : D -> C
9. _ : A -> U{i}
10. _' : D
⊢ =(U{i}; U{i}; U{i})

It may be that I need to change the definition of Psh in order to be able to specify the level:

[Psh(X)] =def= [X -> U{i}].

to

[Psh(U;X)] =def= [X -> U].

In the relevant bits of the agda version I had to do something similar by making the levels explicit. However, even when I make that change and play around with the levels I end up with =(U{i'}; U{i'}; U{i}) or something similar.

I looked at the levels example but I'm not sure how to apply that here.

[jonsterling]

I think that you are experiencing the crappiness of the level inference heuristic. The following proof script works:

  unfold <cmp UpperStar UpperShriek Psh>;
  *{intro @i'; focus 1 #{autoR}}

[Deleted user]

Ah right, I think you mentioned how to do this before but I had forgotten. Thanks, I'll give that a try.

[jonsterling]

I have implemented a fix for this issue, so autoR should now suffice for your proof

[Deleted user]

Nice! Just tried it and indeed it works. Thanks :)