Hi! Is there a reason why there is no "contravariant" variance specifier for universe cumulativity? I'm doing a proof-of-concept predicative church encoding as `Definition nat_r@{i j | j < i} : Type@{i} := forall X : Type@{j}, X -> (X -> X) -> X .`

and it would be useful to me to declare `j`

contravariant.. In fact i can declare just fine the coercion myself by eta-expansion:

```
Definition lower_r@{i0 i1 j0 j1 | j0 < i0 , j1 < i1 , j1 <= j0}
: nat_r@{i0 j0} -> nat_r@{i1 j1} := fun n X => n X .
```

Also i'm not so sure how to properly use explicit universe polymorphism: from my little experience i have had some trouble with using the successor (level `i+1`

) as in `Definition nat_r@{i} : Type@{i+1} := forall X : Type@{i}, X -> (X -> X) -> X `

, but this definition has the advantage of having one less level parameter (which makes subsequent definitions less clutered with tons of parameters and inequalities). Is using `i+1`

discouraged or should i stick with it? (i don't remember precisely but i think in some places like constraints i couldn't write such expressions)

IIRC/IIUC: `i+1`

is an algebraic universe, and I'm no expert but it's been discussed that Coq does not support them well because they increase the asymptotic complexity of type inference/elaboration.

https://coq.zulipchat.com/#narrow/search/algebraic.20universe finds multiple discussions, like

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Universe.20polymorphic.20definition.20with.20unbound.20levels/near/261525227 or https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60False.20.3A.20Prop.60.20vs.20.60Empty_set.20.3A.20Set.60/near/282235398.

Thanks, I didn't know they were part of a different feature! I'll checkout the links!

I think Coq supports contravariance but only for inductive types (see the `Polymorphic Inductive Cumulativity`

flag). I don't know why it's not also supported for constants (though as you note it adds no expressivity power, only performance and convenience (and ease of use of tactics, probably), since it can always be accomplished by delta-expanding the constants, eta-expanding the functions, and making use of inductive cumulativity.)

there is no contravariance in Coq, only eta expansion

see also https://github.com/coq/ceps/pull/47

Last updated: Jun 22 2024 at 16:02 UTC