[Agda] Universes à la Tarski and induction-recursion

[Dan Licata]

> > 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).

I agree that you want this ability.  It's kind of a shame that, while
Martin-Loef type theory is compatible with groupoids and
higher-dimensional categories, there's no way to actually introduce
them!  I think what you would want is a "higher-dimensional quotient
type", where you define a type by writing down a category internally to
the type theory, and then can hook this into the type-generic operations
for identity types, like subst and J.  

I speculated on this a little in Chapter 8 of my thesis:
http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf
though things are little different there, because in my context I was
thinking about types as general categories, not groupoids.  

-Dan