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

[Darryl McAdams]

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
about strick finitism, or general vertigo about the transfinite.

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