[Agda] Equivalence axiom => extensionality

[Dan Doel]

On Tuesday 22 June 2010 12:53:32 pm Dan Licata wrote:
> 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)
> 
> ...

For the benefit of my understanding (and perhaps others')...

Is this a renaming of the notion of equivalence of n-categories?

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