test: Quotient universe levels

[Alizter]

I've added tests to check what the universe levels for quotient are like. Many of them are incorrect in the sense that Quotient takes 3 universe variables, but lemmas about it restrict to 2.

Does it really make sense for Quotient to take 3 levels? There are 2 "real" levels and the third is supposed to be a max of them without restricting the relation between the other two.

[jdchristensen]

I think it is correct for Quotient to take three universe variables. If it weren't for the Trunc, you could remove the universe it lands it and replace it with max applied to the other two, but since we need to apply Trunc, three is needed and is standard for this kind of construction.

However, I noticed that GraphQuotient@{i j u} doesn't enforce that j <= u. I think we should change its universe annotation to @{i j u | i <= u, j <= u} (and we should do the same for Quotient as a form of documentation/testing). Unless I'm confused, a HIT needs to land in a universe that contains both the point constructors and the path constructors. I wonder if other HITs also get this wrong?

I agree that something odd is happening with in_class and other nearby results. I think they should use the same three universes at Quotient. Maybe the easiest fix is to have a Local Definition Q := Quotient@{i j u} R. (or something like that) in the Section?

BTW, I don't think we need a test file for this. I prefer to annotate the definitions themselves when possible, since it provides both documentation and a test.

[jdchristensen]

Should we close this without merging?