Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

One view of homotopy theory is that it replaces the relation "=" (equality) with a looser (but fairly intuitive) notion of path-connectedness. Equality of two points on a topological space is replaced with existence of a path leading from one to the other. Then equality of two continuous functions is replaced with the existence of a path between the two functions lying on a space in which the two functions are points (note that if two functions are equivalent in this sense they are referred to as homotopic, and the exact path is a homotopy). Likewise, the notion of isomorphism, which is usually defined by f o g = id_A and g o f = id_B, is replaced with f o g being homotopic to id_A and g o f being homotopic to id_B. If two topological spaces are isomorphic in this looser sense, then they are said to be homotopy equivalent and the functions f and g are each referred to as homotopy equivalences.

A table comparing equals-based terminology with path-connectedness terminology can help:

- Equality of points : existence of path

- Two functions are equal : two functions are homotopic

- Isomorphism : Homotopy equivalence

- Isomorphic : Homotopy equivalent

There is a formal system called Homotopy Type Theory which exploits the above analogy in a really nice way. It does this by treating path-connectedness as a more fundamental notion than equality, with the former becoming the latter if the topological space is discrete (and therefore essentially a set). HoTT actually can't see equality.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: