A seminar on HoTT Equivalences

I recorded our local Seminar on foundations in which I talked about the notion of equivalence in HoTT:

Hopefully some people will find some use for it. It is pretty slowly going, and it might motivate some of the strange things going on in Equivalences.v.

This entry was posted in Talk. Bookmark the permalink.

5 Responses to A seminar on HoTT Equivalences

Mike Shulman says:

8 December 2011 at 14:32

It’s surprisingly hard to prove that is_equiv and is_adjoint_equiv are equivalent! I end up fooling around with lots of transport along funexts and needing new lemmas about transporting in iterated total spaces, and I’ve never been sufficiently motivated to make it work.

Reply
- Mike Shulman says:
  
  16 December 2011 at 03:00
  
  Well, I finally managed to prove this. I was going about it too directly — turns out it’s easier to massage them both step-by-step through a series of basic equivalences until they come out the same. See this file.
  
  I also finally proved (same file) that the other possible definition, called is_hiso in Equivalences.v, is equivalent to is_equiv. That one is significantly easier. Of course, both proofs use function extensionality.
  
  Reply
  - andrejbauer says:
    
    16 December 2011 at 04:53
    
    Excellent, thank you!
    
    Reply
andrejbauer says:

12 December 2011 at 11:14

And they are equivalent, correct?

Reply
- Mike Shulman says:
  
  12 December 2011 at 12:53
  
  Well, since is_equiv is a prop and we have maps in both directions, their being equivalent is equivalent to is_adjoint_equiv being a prop. That doesn’t seem to be any easier to prove in Coq, but homotopical and higher-categorical intuition says that it’s true.
  
  For instance, we could consider the theory of “marked simplicial sets” in section 3.1 of Higher Topos Theory, which are simplicial sets equipped with a subclass of “marked” 1-simplices denoting “equivalences” (thus a higher-categorical version of “categories with weak equivalences”). Any quasicategory $X$ has an underlying marked simplicial set $X^\natural$ in which all the equivalences are marked, and any simplicial set $A$ gives rise to a marked one $A^\sharp$ in which all edges are marked.
  
  Let $\Delta^1$ denote the 1-simplex, and let $E$ denote a simplicial set such that maps $E\to X^\natural$ consist exactly of the data corresponding to is_adjoint_equiv. Thus $E$ has two 0-simplices $x$ and $y$ , two 1-simplices $f\colon x\to y$ and $g\colon y\to x$ , 2-simplices $g\circ f\to 1_x$ and $f\circ g \to 1_y$ , and one 3-simplex exhibiting one triangle identity between $f$ and $g$ . Then the induced inclusion $(\Delta^1)^\sharp \to E^\sharp$ is “marked anodyne” ( $E$ can be obtained from $\Delta^1$ by gluing on two horns). Since the fibrant marked simplicial sets are just the objects $X^\natural$ for $X$ a quasicategory, this implies that the induced map of simplicial sets $Map(E^\sharp,X) \to Map((\Delta^1)^\sharp,X)$ is a trivial fibration. Hence, any equivalence in a quasicategory $X$ has a contractible space of extensions to adjoint equivalence data (the corresponding fiber of this map).
  
  Reply