[Agda] Equivalence axiom => extensionality

[Peter LeFanu Lumsdaine]

> On Tuesday 22 June 2010 12:53:32 pm Dan Licata (mostly) wrote:
>> A is contractible if for all M N : A, Id_A(M,N)
[Dan called it connected, not contractible]
>> 
>> A is a 1-Set if it's hom sets (identity types) are contractible:
>>  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 contractible:
>>  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)
>> ...

On 29 Jun 2010, at 01:22, Dan Doel wrote:
> For the benefit of my understanding (and perhaps others')...
> 
> Is this a renaming of the notion of equivalence of n-categories?

Yep --- or at least of the n-categories themselves, not the notion of equivalence.  Maybe this is a good place to go into more of the background to this thread:

This terminology comes from the (still partially conjectural) model of types as weak-\omega-groupoids (or homotopy types, simplicial sets, spaces, etc.)  Dan and I met this particular hierarchy of definitions when Voevodsky visited Pittsburgh last year to talk about it.

The idea is that among the weak-\omega-groupoids are the weak-n-groupoids; and an "n-Set" is a type which is (equivalent to) an (n-1)-groupoid.  So:

0-Set = (-1)-groupoid = truth-value = all hom-sets contractible = contractible-if-inhabited.

1-Set = 0-groupoid = set = all hom-sets are truth-values

2-Set = groupoid = all hom-sets are sets

etc. etc.

The subtle/surprising (to me) point is that the definition of "contractible" _looks_ like it's just a definition of "connected".  But because all operations are interpreted "continuously"/"(weakly) naturally", it interprets as "continuously connected", i.e. "contractible".  (This is provable in the type theory: "contractible" implies "all hom-sets contractible", which reasonably justifies why that's a better name than just "connected".)

The interesting thing now is that --- because of this same subtlety, that the interpretation is on the one hand "weak" but on the other hand always "natural" w.r.t. identity types --- we _don't_ have to use a co-inductive definition of equivalence like you describe below!  If we just write down the standard internal definition of isomorphism (maybe better called "weak equivalence" in this setting, to keep consistent with the interpretation):

WkEquiv : (A B : Set) → Set
WkEquiv A B = Σ (A → B) (λ f → 
                Σ (B → A) (λ g → 
                Σ ((a : A) → (a ≡ (g (f a)))) (λ η → 
                ((b : B) → ((f (g b)) ≡ b)))))

then this is interderivable with various other subtler (coinductive etc.) definitions of equivalence one can define.

While it's interderivable, though, it's not quite equivalent to them!  --- if we bump it up slightly, by adding a term witnessing one of the triangle inequalities

OneTriEq : (A B : Set) → Set
OneTriEq A B = Σ (A → B) (λ f → 
                Σ (B → A) (λ g → 
                Σ ((a : A) → (a ≡ (g (f a)))) (λ η → 
                Σ ((b : B) → ((f (g b)) ≡ b)) (λ ε →
                  (a : A) → trans (ε (f a)) (cong f (η a)) ≡ refl))))

then this has the nice property that for any f, the obvious type IsOneTriEq(f) is a 0-Set ("contractible-if-inhabited"); IsWkEquiv(f) is interderivable with IsOneTriEq(f), but may not be equivalent to it, as IsWkEquiv may not be a 0-Set (without the triangle inequality, there is some "homotopical freedom" in the choices of η and ε).

Alternatively, if you write down an internal definition of (in the usual interpretation) "bijection", i.e. "the inverse image of any point is a singleton", or in the language of this interpretation, "the homotopy fiber over any point is contractible", you get something again _equivalent_ to IsOneTriEq.  This was the definition of "equivalence" that Voevodsky was using.

He then proposed the "equivalence axiom" (I don't think he was the first to propose something like it, but others on this list probably know that better than I?): that "equality is equivalence", i.e. that the natural map

Id X Y   →   Equiv X Y

is _itself_ an equivalence (where Equiv is one of the strong notions above).

Cheers,
-p.

> That being something like:
> 
>  The proper notion of equivalence of objects in a (1-)category is
>  isomorphism. And Set is a category (1-sets form a category).
> 
>  The proper notion of equivalence in a 2-category is isomorphism of 0-cells
>  up to isomorphism of 1-cells. And equivalences of (1-)categories are given
>  in the 2-category of 1-categories.
> 
>  etc. (cue hand waving)
> 
>  In infinity-categories, equivalence of n-cells is given by a pair of
>  (n+1)-cells that are inverses up to (n+1)-cell equivalence.
> 
>  (1-)Sets are 0-categories
>  Connected/contractible sets are (-1)-categories.
> 
> -- Dan
> 

-- 
Peter LeFanu Lumsdaine
Carnegie Mellon University