There are subtleties here, when type annotations are present, depending in quite a brittle way on where they must be placed. (I'm half-remembering conversations about this with Zhaohui Luo.) Suppose we demand (as many do) type annotations on lambda, with a typing rule like this
S : Type_i x : S |- t : T
-----------------------------
\ x : S -> t : (x : S) -> T
In particular, we may readily have
\ X : Type_1 -> X : (X : Type_1) -> Type_1
Now, if cumulativity were contravariant in the input type, we should allow
(X : Type_1) -> Type_1 <= (X : Type_0) -> Type_1
and, indeed, one might imagine that the identity function for Type_1
should work perfectly well for those of its inhabitants which happen also to live in Type_0
. But there's a snag, if you want cumulativity to be, in a suitable sense, reducible to universe inclusion. The typing rule for lambda will only ever give
\ X : Type_1 -> X
function types with the domain Type_1
, because that is what the domain type annotation says, and we're stuck with it. There is a function that does thejob we want, but it's
\ X : Type_0 -> X
and that ain't the function we first thought of.
Now, if you're me, you arrange never to synthesize the types of lambda abstractions, only to check them, removing the need for the type annotation. Then, both Type_0 -> Type_1
and Type_1 -> Type_1
will accept \ X -> X
. In the bidirectional setting, the "change of direction" rule says that to check that T
accepts a term whose synthesized type is S
, then an S
thing should be able to do all a T
thing's jobs. That clear directedness yields great temptation to relax from equality to a subsumptive notion of subtyping, and in that setting contravariance in function domains is not a problem.
A1
is not equivalent toA2
then the whole thing becomes very confusing to me. AFAIU the marked rules assume thatB1
depends onx : A1
whileB2
depends onx : A2
. Now ifA1
andA2
are different types how can we compareB1
andB2
at all? In particular, what needs to be added to the contextx : A1
orx : A2
to even correctly construct bothB1
andB2
to compare them? $\endgroup$B1 : A1 -> Type
andB2 : A2 -> Type
such thatA1 <= A2
. Then in the contextx : A1 |-
we can easily compareB1(x) <= B2(x)
becausex:A1
is coerced to an element ofA2
. So there is no problem here. $\endgroup$A2 ≤ A1
for contravariance. :) But the perspective to have a function type that's a subtype of another function type only on a subset of its domain is still puzzling and a bit unnerving to me. :D $\endgroup$i : A2 >-> A1
and a family of injective functionsjx : B1(ix) >-> B2x
then there is an obvious injective functionPi(A1,B1) >-> Pi(A2,B2)
. I find it hard to understand what can be more natural than this... $\endgroup$