The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi all,

I have a question about dependent function types and universe subtyping.

Coq has this rule:

"if E[Γ] ⊢ T =βδιζη U and E[Γ::(x:T)] ⊢ T′ ≤βδιζη U′ then E[Γ] ⊢ ∀ x:T, T′ ≤βδιζη ∀ x:U, U"

Seen here in point five.

The bit that I want to know more about is why we need T = U and not T => U. That is, why is this rule not contravariant on the domain of dependent function types?

In the OPLSS 2011 slides (slide 23), for CoC with a universe hierarchy, we also don't have contravariance over the domain. Yet I've seen other PTS definitions (typically without universes, so I'm not sure if the distinction lies there) which define subtyping in a way that is contravariant for this rule.

I'm curious if this is a deliberate decision since I can't find much about it. That is, would being contravariant over the domain break anything? If so, what in particular? If not, is there a reason that Coq doesn't allow this?

Thanks!

Talia