Questions tagged [subtyping]

Use this tag for polymorphism that restrict the range of types that can be used in a particular case.

Filter by
Sorted by
Tagged with
9 votes
2 answers

What's the benefit of having pi and sigma types with an invariant parameter?

Ulf Norell wrote this in his PhD thesis (figure 1.6): This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda ...
ice1000's user avatar
  • 5,802
5 votes
1 answer

What subtyping rules does Agda support?

Andrea Vezzosi said Cubical Agda made cubical subtyping coercion-based (inS and outS) because it's a bad idea to introduce more ...
ice1000's user avatar
  • 5,802
14 votes
2 answers

Formal description of algorithmic subtyping/cumulativity

Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the ...
ionchy's user avatar
  • 906