Re: [Agda] Universes à la Tarski and induction-recursion

[Thorsten Altenkirch]

On 2 Feb 2011, at 07:11, Peter Dybjer wrote:

> Personally, I have a position on the "closed vs open universe" issue, but I don't have time at the moment to expand on it. Anyway, it's philosophy.

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

They are two different beasts. As noted by Dan, in U we can do type-case but in Set we can't. To compensate for this we may add parametricity to Set (theorems for free) but it would be unsound to do so for U. 

This is similar to the story for functions. we may represent functions as codes, in which case we can analyze their definition, and hence extensionality would be unsound or we have proper functions and the only thing we can do is to apply them. In this case extensionality can be added (and should unless you suffer from masochism).

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.

I am wondering wether there is a relation between Voevodsky's axiom and parametricity because both state that sets are extensional. 

Cheers,
Thorsten