5
$\begingroup$

Andrea Vezzosi said Cubical Agda made cubical subtyping coercion-based (inS and outS) because it's a bad idea to introduce more subtyping relations which complicates the system. Also Agda did not have cumulative universes (it is added now).

So does Agda support any subtyping relations? Without using rewriting and cumulativity options of course.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

The current subtyping rules that Agda uses are for sized types (when --sized-types is enabled) and cumulativity (when --cumulativity is enabled). Currently neither of these options are allowed under the --safe flag, so with --safe there is no subtyping in Agda.

There used to be subtyping rules for irrelevant and erased function types as well, but these were removed recently (see This successful Pull Request which was merged into Master on GitHub) because they were causing performance problems and anyway only save the user a simple eta-expansion.

Improve this answer
$\endgroup$
1
  • $\begingroup$ What kind of subtyping does Agda have for sized types? Is it the kind that uses polarity annotations on (co)inductives? $\endgroup$
    – ionchy
    Commented Mar 29, 2022 at 19:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.