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.

About these ads
This entry was posted in Talk. Bookmark the permalink.

5 Responses to A seminar on HoTT Equivalences

  1. Mike Shulman says:

    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.

    • Mike Shulman says:

      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.

  2. andrejbauer says:

    And they are equivalent, correct?

    • Mike Shulman says:

      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).

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s