[Agda] Equivalence axiom => extensionality

[Dan Licata]

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