You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Suraaj K S (Dec 01 2024 at 10:12):I was playing around with the coq theorem prover. If I understand correctly, coq's core type theory has an infinite hierarchy of universes Set, Type1, Type2, Type3, ....
My question boils down to what type the following inductive definition has:
Inductive mydata (X:Type) : Type :=
| inj (x:X).
Check mydata. (* :Type@{mydata.u0} -> Type@{mydata.u0} *)
Here, if I understand correctly, mydata.u0 is a 'universe 'meta-number', and coq will typecheck successfully as long as it can assign concrete universe numbers (and there might be many such assignments) such that you can construct a typing derivation (according to Galina's core calculus)? For instance, one possibility is Set -> Set in this case.
Informally, it seems like some kind of 'meta'-level polymorphism, and I was wondering if this technique is well-known / has a name? Also, is my understanding correct that the core calculus does not talk about these 'universe number' metavariables, and the unification mechanism is built on top of it? I'm curious if it is possible, to forcefully pin a universe number as well (Although I'm not sure when this would be useful)
Nathanael Arkor (Dec 01 2024 at 10:36):There's a Coq Zulip, which would be a better place to ask this sort of question.