Stream: Coq users

Topic: ✔ Proper vs. Set

view this post on Zulip Karl Palmskog (Jul 22 2023 at 14:16):

The Proper machinery/classes are available both for Prop and Type, but (to my knowledge) not for Set. Is there an obvious reason why? One would think that Proper for Set would be nice with -impredicative-set, but I'm guessing this is very niche.

view this post on Zulip Gaëtan Gilbert (Jul 22 2023 at 14:27):

the Type side is univ poly so can be instantiated at Set

view this post on Zulip Notification Bot (Jul 22 2023 at 14:46):

Karl Palmskog has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC