# [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")

Mon Jul 1 22:26:49 CEST 2013

```What I mean by thing is a thing in the model. Judgements, at least, aren't taken to be things in the model, but are, as far as I know, apart from it. They're merely ways of talking about things. So why not treat levels similarly? I'm partly inspired by Boolos's reworking of second order logic to be "merely" syntactic -- he replaced sets and set membership with a variable assignment relation (on top of the assignment function) in the model theory, so that "set" membership is just being related to a variable. There are no sets in Boolos's pseudo-MSO logic, but it looks a lot like there are because of a syntactic trick. So why not do something similar with levels?

- darryl

________________________________
From: Peter Hancock <hancock at spamcop.net>
To: Darryl McAdams <psygnisfive at yahoo.com>
Cc: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
Sent: Monday, July 1, 2013 3:33 PM
Subject: Re: [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")

On 01/07/2013 19:58, Darryl McAdams wrote:
> Do levels really have to be things at all?

Well, I'm not sure what a thing is, but I think I agree with you,
if things are elements of sets.

> If we think of levels as
> merely/purely syntactic elements of the type theory, then it seems
> like the relational judgment "type_n" that Martin mentions would
> sidestep the issue entirely.

Aren't natural numbers things?  There's a set of them.  Natural
numbers aren't syntactical.

>Levels would no more exist in the model
> then ":" and "valid-context" do. - darryl

My favourite natural number (after zero) is 1.  It is impervious to arguments

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?

Hank
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130701/18242a52/attachment.html
```