Stream: Coq users

Topic: Coerce list Set to list Type


view this post on Zulip Lef Ioannidis (Feb 10 2022 at 17:44):

Why can I coerce Set to Type but not list Set to list Type, I thought list was covariant. Am I misunderstanding how universe polymorphism works?

Definition bar : Type := nat.
Fail Definition foo: list Type := [nat; nat].

On the other hand, this works so perhaps this is just a syntactic quirk or some global setting I can use to enable this coercion

Definition foo': list Type := [nat: Type; nat: Type].

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 17:48):

Set and Type are arguments, not universe arguments, so univ poly is irrelevant
[nat] is elaborated to @cons Set nat (@nil Set) which is a list Set
[nat : Type] is elaborated to @cons Type nat (@nil Type) which is a list Type

view this post on Zulip Lef Ioannidis (Feb 10 2022 at 17:51):

Right, I guess my question is; what are the coercion rules? Obviously a coercion happens in bar and foo' but not in foo. I assumed it is standard covariance rules but maybe I am wrong?

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 17:51):

this is cumulativity not coercion

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 17:55):

the rules are at https://coq.github.io/doc/master/refman/language/cic.html#subtyping-rules

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 17:58):

see also https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Difference.20between.20Set.20and.20Type


Last updated: Jan 28 2023 at 07:30 UTC