Janno (Jun 05 2020 at 11:29): 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?
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.
Janno (Jun 05 2020 at 11:31):Got it! Thanks. (It's very confusing.)
Gaëtan Gilbert (Jun 05 2020 at 11:31):It's a kinda gnarly behaviour which I'm not sure how to describe exhaustively.
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
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: Oct 13 2024 at 01:02 UTC