[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

I have played around a bit with weak equality trying to compare it
with isomorphism. In particular I tried to see what extra condition
weak equality corresponds to.

Given f : A → B and g : B → A we have

ε : (b : B) → f (g b) ≡ b
η : (a : A) → a ≡ g (f a)

which means that A and B are isomorphic.

I would expect that I get the equations corresponding to saying that ε
and η are an adjunction between groupoids (I think this was also what
Peter Lumsdaine suggested when he was in Nottingham):

α : ε (f a) ∘ f (η a) ≡ id
β : g (ε b) ∘ η (g b) ≡ id

However, when translating the condition corresponding to weak
equivalence I get: Given e : f a ≡ b

δ e : ε b ∘ f (g e ∘ η a) = e

Clearly the first equation is a consequence setting b = f a and e =
refl. But I don't see how the other equation would follow (and I don't
think there are interderivable).

Also I don't see that this enough in higher dimensions. Shouldn't we
expect equations relating α and β or δ?

An alternative would be to use equality of sets to express the
adjunction:

γ : (f a ≡ b) ≡ (a ≡ g b)

This may be a bit recursive (since we now define equality of sets via
equality of sets) but some progress seems to be happening since we are
now going one dimension up.

Cheers,
Thorsten