[Agda] Equivalence axiom => extensionality

[Peter LeFanu Lumsdaine]

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