[Agda] Yet another questions about equality

[Dan Doel]

On Sunday 27 February 2011 8:04:42 AM Thorsten Altenkirch wrote:
> The latter is easily broken in conventional set theory. I.e. neither union
> nor intersection are stable under isomorphism (And there were suggestions
> to introduce this sort of operations into Type Theory. The basic intuition
> in Type Theory is that you have to construct the set before you can
> construct any of its elements, while in Set Theory the elements are there
> first and the sets come later. Univalence is a consequence of this
> principle.

This paragraph worries me a little. Because I'm a little interested in certain 
types of unions/intersections.

That is, if Agda ever gets it:

  .(x : A) -> B x

can be thought of as the intersection of the B family. And:

  data U (A : Set) (B : A -> Set) : Set where
    _,_ : .(x : A) -> B x -> U A B

is a union. Conceivably, if B a = B a' (equality, not isomorphism), and b is 
an element of that type, then we should grant (a, b) = (a', b). And this of 
course erases to b = b.

So, should I be worried? I guess I can see a problem. If B a is merely 
isomorphic to B a', then it seems like we might be roped into a situation 
where we need to consider (a, b) and (a', b') equal if b corresponds to b' in 
said isomorphism between B a and B a', which sounds dangerous. Indeed, there 
can easily be more than one such isomorphism, so which bs do we choose to be 
equal to one another?

-- Dan