Stream: Coq users

Topic: Singleton Inductives


view this post on Zulip Janno (Jun 05 2020 at 11:29):

Why does Record unit_set : Set := tt_set { }. Check unit_set. return Set when
Record unit_type : Type := tt_type { }. Check unit_type. returns Prop? Is there something special about Set that makes it illegal to consider unit_set a Prop?

view this post on Zulip Gaëtan Gilbert (Jun 05 2020 at 11:30):

No, it's Type (the syntax) which is considered specially by Inductive/Record and automatically lowered as much as possible.

view this post on Zulip Janno (Jun 05 2020 at 11:31):

Got it! Thanks. (It's very confusing.)

view this post on Zulip Gaëtan Gilbert (Jun 05 2020 at 11:31):

It's a kinda gnarly behaviour which I'm not sure how to describe exhaustively.

view this post on Zulip Bas Spitters (Jun 05 2020 at 11:53):

Does this help, or make it more confusing?
https://golem.ph.utexas.edu/category/2012/12/universe_polymorphism_and_typi.html
https://ncatlab.org/homotopytypetheory/show/universe

view this post on Zulip Janno (Jun 05 2020 at 12:01):

I don't think these posts actually get to the core of my question. I am familiar with Coq's handling of universes (to the point where I sometimes wish I knew less about it) and I also knew that it lowers singleton Types. I just didn't know why Set didn't get the same treatment.


Last updated: Jan 29 2023 at 01:02 UTC