[Agda] Yet another questions about equality

[Conor McBride]

On 27 Feb 2011, at 13:52, Dan Doel wrote:

> 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

These days, I'm made nervous the moment I see

   I : (X : Set) -> X -> X -> Set

as it makes the proposability of an equation contingent on the  
definitional,
equality, which should is basically some kind of grotesque accident.

I suppose if you've got some small universe

   El : U -> Set

and you close I U under isomorphism, then what does J do? It certainly  
allows
us to define

   coerce : (A B : U)(I U A B) -> El A -> El B

which I suppose, in the case that the proof of I U A B is by  
exhibiting a
weak equivalence, must actually deploy the given function, if it's to  
mean
anything at all, computationally. For "pragmatic" reasons, I like  
computation
to work. Obviously, if I was more principled, I'd be happy to break it.
Anyhow, we can construct

  Iupto (A B : U)(Q : I U A B) -> El A -> El B -> Set
  Iupto A B Q a b = I (El B) (coerce A B q a) b

and go from there. It *should* make sense to propose equality of  
elements
in demonstrably equal sets (and the meaning of that proposition will  
depend
on the demonstration. E.g., if A = B = Bool, then which pairs a and b  
in Bool
are thus related will depend on whether Q is given by id or by not.

Does that give us a basis to think about (small) intersections and  
unions?

Cheers

Conor