[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

On 22 Jun 2010, at 19:02, Peter LeFanu Lumsdaine wrote:

> (feel free to forward part or all of this to the Agda list, I'm not a subscriber yet so am not sure whether to do so)
> 
> Yep, the hierarchy numbering is how I remember it!  but I think we were calling it "contractible" not "connected", to emphasise the fact that while it _looks_ like it just means "connected", it actually interprets as (and generally behaves more like) "contractible"?
> 
> One terminology question, btw: I guess you're using "weak equivalence" in VV's sense; but what precisely do you mean by "isomorphism" and "bijection"?  (sorry --- I'm still not quite familiar enough with some of the type-theoretic conventions here!)

Actually, I thought this has nothing to do with Type Theory....

Two sets A,B are isomorphic if there are functions f : A → B and f' :
B → A, which are inverse to each other. A and B are bijective (one
says equinumerous but this I find misleading) if there is one function
g : A → B which is both injective and surjective, i.e. both monic and
epic.

Clearly, isomorphic implies bijective but the other way around seems
not provable constructively, afaik. From surjective you get an iverse 
g' : B → A such that g ∘ g' = id but not the other way
around. Injectivity doesn't give you a function, but even if you
assume that it is split (or what is the word) you just get another
function g'' : B → A, such that g'' ∘ g = id but I don't see why g'' =
g' or how you could in general construct one function which is both
left and right inverse to f. Or am I overlooking something obvious?

Classically, if we view functions as functional relations it is easy
to see that given a bijection R : A → B → Prop then its relational
inverse R' : B → A → Prop is a function and R, R' constitute an
isomorphism.

Moreover, at least with respect to the formalisation of weak
equivalence I did with Thierry (I attach again), it is clear that
propositionally weakly equivalent is the same as bijective. The fiber
of f is just the the inverse and saying that the inverse is
contractive, i.e. has precisely one element is clearly the same as
bijective.

Hence, I don't think that isomorphic and weakly equivalent are the
same even if we ignore higher dimensions.

Cheers,
Thorsten

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Equivalence.agda
Type: application/octet-stream
Size: 1108 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100623/3114861e/Equivalence.obj
-------------- next part --------------

> 
> Thanks for cc'ing me in!  This is nice to think about again :-)
> -p.
> 
> That numbering of the hierarchy
> On 22 Jun 2010, at 18:53, Dan Licata wrote:
> 
>> Hi Thorsten,
>> 
>> As I understand it, weak equivalence is the same as isomorphism for any
>> Set, by which I mean a type that has UIP: 'A' is a set if for all p, q :
>> Id_A(M,N) , Id_(Id_A(M,N))(p,q).  I think this is called a 1-Set, though
>> I often screw up the indexing of the hierarchy (I'm CC'ing Peter
>> Lumsdaine, who can correct me if I'm misremembering the definitions
>> here):
>> 
>> A is connected if for all M N : A, Id_A(M,N)
>> 
>> A is a 1-Set if it's hom sets (identity types) are connected:
>> for all M, N : A, for all p, q : Id_A(M,N) , Id_Id_A(M,N)(p,q)
>> 
>> A is a 2-Set if it's hom sets' hom sets are connected:
>> for all M, N : A, for all p, q : Id_A(M,N) , 
>>     for all a , b : Id_Id_A(M,N)(p,q) , Id_(Id_Id_A(M,N)(p,q))(a , b)
>> 
>> ...
>> 
>> 
>> I think the idea is that weak equivalence gives you the appropriate
>> notion of equivalence for each level in the hierarchy.  So to show that
>> two 1-Set's are equal, you show that they are isomorphic.  But to show
>> that two 2-Set's are equal, you can additionally show that they are
>> isomorphic up to isomorphism.
>> 
>> For example, Unit (or any proposition, in the OTT sense) is connected
>> (all terms are equal).  
>> 
>> Nat is not connected (0 != 1), but it is a 1-Set (Id_Nat just contains
>> identities).
>> 
>> On the other hand, Agda's 'Set' would be a 2-Set, with members A, B :
>> 1-Set, and Id_Set(A,B) being isomorphisms between A and B.  So it is not
>> a 1-Set, because not all isomorphisms are equal.  But it is a 2-Set,
>> because the only map between two proofs that two isomorphisms are the
>> same is the identity.  
>> 
>> So an example of a weak equivalence but not an isomorphism would go like
>> this: construct two universes Set and Set' of 1-Set's, which are each a
>> 2-Set, such that they are not isomorphic, but they are isomorphic up to
>> isomorphism.  I.e.
>> 
>> whenever you can write 
>> 
>> f : Set  -> Set'
>> g : Set' -> Set
>> 
>> that transform the types back and forth they don't compose to the
>> identity on the nose: It's not the case that
>> 
>> A |- f (g A) = A
>> A |- g (f A) = A.
>> 
>> But there are such an f and g that compose up to isomorphism:
>> 
>> A |- f (g A) \iso A
>> A |- g (f A) \iso A
>> 
>> -Dan
>> 
>> 
>> 
>> 
>> 
>> On Jun22, Thorsten Altenkirch wrote:
>>> Hi Dan,
>>> 
>>> thank you for this clear explanation.
>>> 
>>> Indeed, for finite sets weak equivalence (i.e. a bijection) is the
>>> same as isomorphism. And as you say if you identify all isomorphisms
>>> on Bool you are in trouble.
>>> 
>>> An alternative to "weak equivalence" would be isomorphism. Certainly
>>> isomorphism implies weak equivalence but not vice versa (for infinite
>>> sets). Does the proof of extensionality rely on using weak equivalence
>>> or would it work for isomorphism as well?
>>> 
>>> What are weak counterexamples for sets that are weakly equivalent but
>>> not provably isomorphic?
>>> 
>>> To me weak equivalence looks very classical. I am a bit puzzled that
>>> this should be the right notion for equality of sets.
>>> 
>> 
> 
> -- 
> Peter LeFanu Lumsdaine
> Carnegie Mellon University
>