[Agda] Universes à la Tarski and induction-recursion

[Dan Doel]

On Wednesday 02 February 2011 2:11:02 AM Peter Dybjer wrote:
> Let me just tell you my recollection of discussions with Martin-Löf and
> colleagues here in Gothenburg in the 1980s.

Thanks, it was interesting (didn't want to clutter the list with just that).

On Thursday 03 February 2011 7:07:58 AM Thorsten Altenkirch wrote:
> Is this necessary? In my view we have both: open universes (e.g. Set_i) and
> closed universes (like the U,T given by Dan using induction-recursion).
>
> ...
>
> Actually, Voevodsky's univalence axiom (weakly equivlalence of sets is
> weakly equivalent to set equality) is related: It only works for an open
> universe, since it implies that we can exchange isomorphic sets. In this
> sense this axiom is a rather strong extensionality principle.

Yes. I've been thinking about this some recently (who hasn't). And the 
difference crystalized a bit yesterday. Induction-recursion (and every other 
inductive formation, and probably others) lets us define new _sets_ (in the 
univalent sense). The inhabitants of a set are unique up to equality.

There is no way, however, to define (ex-nihilo) a new geinuine _category_ in 
Agda. The built-in Set (n) is all there is. Sets can be promoted to 
categories, by taking an existing set as the collection of objects and 
equipping that with arrows. But the rigorous category theorist will tell you 
that in general we shouldn't think about the _set_ of objects of a category, 
and as a consequence, we should only be able to talk about the objects of a 
category up to isomorphism. We can choose to work that way for any set, but it 
is only enforced (to any degree) for Set (and I suppose types that contain one 
or more Sets).

So perhaps in a language of the future, it will be possible to define both new 
sets and new (n-)categories, in which case closed universes would be defined 
as sets, and open universes would be categories (or something along those 
lines).

-- Dan