[Agda] Yet another questions about equality

[Thorsten Altenkirch]

Good point. 

Dependent irrelevance may well be an intensional property. I think we can have both: intensional types live in a closed universe where we can have universe elimination and univalence certainly doesn't apply and open universes where we don't have universe elimination but get some mileage from this by univalence. So maybe dependent irrelvance makes only sense for closed universes.

Thorsten

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
> 
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda