[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

I normalized the types (by Hand) using AC and it seems to me that one
can even formulate a binary WeakEquiv(f,g) which looks as follows
(given f : A → B, g : B → A):

ε : (b : B) → f (g b) ≡ b
α : (b : B)(a : A) → f a ≡ b → a ≡ g b
Å : (b : B)(a : A)(β : f a ≡ b) → f (α β) ∘ ε b ≡ β

I also noticed that if we ignore the last, 2nd order equality then the
first two are actually isomorphic to isIso(f,g) - w.o. UIP obviously.

And as I already remarked this seems to be equivalent to adding

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

to isIso. And δ seems isomorphic to the 1st triangle equality. 

I know understand why the triangle equations are interderivable, here
we have to exploit the fact that we actually have a groupoid (this is
not true for categories in general).

What isn't clear to me is wether this is enough at higher dimensions?
Did you actually claim this?

Cheers,
Thorsten
On 25 Jun 2010, at 09:06, Peter LeFanu Lumsdaine wrote:

> Unfortunately I don't have enough time today code/write up the details of this (I'll try to tomorrow), but we discussed this in Pittsburgh a bit and I think worked out the situation fairly well:
> 
> Iso(X,Y) and WkEquiv(X,Y) _should_ be interderivable (i.e. there are maps going back and forth between the two); they are "the same" in that sense.
> 
> Indeed, for a given f, IsIso(f) and IsWkEquiv(f) should be interderivable.
> 
> However, this _shouldn't_ be a homotopy equivalence: IsWkEquiv(f) is designed so that it should be a proposition (i.e. contractible if inhabited), whereas IsIso(f) isn't quite.
> 
> More specifically, given (g, ε, η), there's some redundancy in the data, making the type potentially non-trivial.  We can compare ε to "η transported across the equivalence", and these might not be the same.  Adding either triangle equality fixes that.  Adding _both_ the triangle equalities introduces redundancy again: we can transport the witness for one across and compare it with the witness for the other, and they might not be equal!
> 
> (So I am claiming, btw, that the triangle equalities are interderivable; essentially, as soon as we have the basic data (f, g, ε, η) of the iso, we should be able to "transport anything across it" in a broad enough sense to include this, I think.)
> 
> So... that's why having no triangle equality, or both, is not quite right.  I don't have a good intuition for why having _just on_ should be the Goldilocks spot --- but I'm pretty sure we proved that(*) in Pittsburgh, and hopefully we should be able to do so again :-)
> 
> (*): so the precise statements I'm claiming are that if we have
> 
> IsWkEquiv(f)
> IsIso(f)
> IsIsoOneTri(f)
> IsIsoBothTris(f)
> 
> then 
> 
> (a) all of these are interderivable,
> and
> (b) IsWkEquiv(f) and IsIsoOneTri(f) are isomorphic.  
> 
> -p.
> 
> 
> On 24 Jun 2010, at 23:47, Thorsten Altenkirch wrote:
> 
>> 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
> 
> 
> -- 
> Peter LeFanu Lumsdaine
> Carnegie Mellon University
>