10 votes
Accepted

What subtyping rules does Agda support?

The current subtyping rules that Agda uses are for sized types (when --sized-types is enabled) and cumulativity (when ...
Jesper's user avatar
  • 486
8 votes

Formal description of algorithmic subtyping/cumulativity

See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.
Andrej Bauer's user avatar
  • 8,621
8 votes
Accepted

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

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 ...
pigworker's user avatar
  • 771
5 votes
Accepted

Formal description of algorithmic subtyping/cumulativity

For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

Why inductive types (or variants) are so rigid in terms of the set of constructors

There are two components to your question. The first, corresponds to the idea of constructor subtyping (actually, non-empty lists are the first example of the paper). I don't think there are any hard ...
Meven Lennon-Bertrand's user avatar
4 votes

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

As pointed out in the comments already, even if you do allow for cumulativity (in one direction or the other) in your domain type, you do not need to record the two types in your context: only the ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible