[Agda] How does level polymorphism fit into a valid type theory?
(from "More universe polymorphism")
guillaume.brunerie at gmail.com
Mon Jul 1 21:48:43 CEST 2013
On 2013/7/1 Peter Hancock <hancock at spamcop.net> wrote:
> Why don't we just have one universe of Sets, memebership of which we express
> by a judgement, that is not a Set-inhabitation judgement, perhaps
> "A is a Set"? Then among the sets, we can have universes like
> Gothendieck's, and index them by whatever mathematical things we like?
Is this universe of Sets supposed to be a term (then what’s its type?)
or a type (then what’s the difference between "A is a Set" and "A :
Set") or nothing?
I guess it’s neither a term nor a type, but then the judgment "A is a
Set" is what I call "A type" and the question is how to index the
universes among the sets.
More information about the Agda