Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > nLab General Discussions: Homotopy hypothesis

Bottom of Page

1 to 45 of 45

  1.  
    • CommentRowNumber1.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 13th 2015
    • (edited Feb 16th 2015)

    (13th February 2015)

    I would like, in a series of comments in this thread, to outline a proof of the homotopy hypothesis, in a very strong sense, for a certain algebraic, cubical notion of ∞\infty-groupoid. I have been working on this kind of question for around four and a half years, and the rough outline of the approach that I will take dates from the beginning of this time. In the years since, when time has permitted, I have been working on placing the approach in a conceptual framework, reworking aspects of it accordingly, and on certain details. Recently, I have felt that I now understand the story deeply enough to wish to make the details public, and have clarified the conceptual points that I wished to address.

    It is likely, however, that writing this up in a conventional way will take me a very long time. This is principally because I wish to write it up in a way which follows my own ’philosophy’ as to how best to approach it. This has a considerable foundational aspect: it is important to me to work constructively, in a strong sense, and I actually wish to work in a formal ’synthetic category theory’, which I am implementing as a Martin-Löf type theory in Coq. This ’synthetic category theory’ differs quite considerably from ’standard’ approaches to categorical foundations, even in the treatment of basic aspects. Thus it will take a considerable time before it is developed even to the point of being able to carry out the work on the homotopy hypothesis that I will describe.

    In this series of posts, at least for a considerable time, I do not plan to emphasise these foundational aspects. I instead plan to focus on the principal ideas which relate directly to the homotopy hypothesis.

    This ’philosophy’ also has a ’stylistic’ aspect. I like to argue very diagramatically, and I like to give full details. Sometimes I also like to write up material in the literature, if it fixes notation, or if I feel that my presentation differs in ways that I prefer. All of these points differ from the sylistic conventions of ’standard’ write ups, and tend to mean that my write ups are quite long.

    Secondly, the work on the homotopy hypothesis has evolved into a broader programme investigating the foundations of abstract homotopy theory: ways to construct derivators; ways to construct model categories, and a reworking of this notion; a cubical Milnor theorem; etc. All these aspects also need to be written up to present fully the work on the homotopy hypothesis as I see it. This is a considerable task, and is not linear: the projects are inter-related. Thus I feel somewhat constrained and daunted by the task of writing it up in a conventional way. In addition, I am interested in other things, which also need writing up, some of which I have mentioned on the nForum before.

    Thirdly, I do not have so much time to work on the writing up. I put a great deal of energy into teaching, and enjoy and am very motivated by it. I feel an ethical responsibility (my apologies if this sound pretentious, I do not intend it to be perceived this way!) to prioritise it over research when the two must be balanced, and do so. Whilst I happen to have a little more time than usual for a few months just now, it is quite possible that I will not have much time, possibly very little time at all, for intensively writing up work in the foreseeable future afterwards. Thus I would prefer to just write up things here and there where I can.

    The reason that I propose to post my work here in the nForum is that I see it as a place in which a community can discuss mathematics related to category theory and higher category theory. I appreciate that the nForum was originally intended as a support for the nLab, but I hope that it now can be considered in a broader light. Indeed, I should say from the beginning that I do not have any particular intention myself to incorporate anything that I write into the nLab (this is of course not to preclude others from doing so, if they so wish and feel that it fits), and that nothing to do with the nLab is, directly at least, part of my motivation for posting here. If the kind of contribution that I have in mind is not welcomed, because a stricter interpretation of the purpose of the nForum is upheld, or for any other reason, just let me know.

    My principal hope is that people will ask questions, and engage in discussion with me, about the ideas that I will post (just post comments in between mine). This would help me enormously with regard to spurring me on to write up more.

    As a final, quick caution, I should say that I do not intend my posts to be viewed as presenting the mathematics ’from on high’. I hope we can agree that arriving at a ’bug free’ presentation of mathematical ideas is a more organic process, and that details are likely to be tweaked in the light of discussion.

    • CommentRowNumber2.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 13th 2015
    • (edited Mar 16th 2015)

    (13th February 2015)

    I’ll begin by working towards a definition of a cubical analogue of the Ex ∞\mathsf{Ex}^{\infty} functor for simplicial sets. This cubical Ex ∞\mathsf{Ex}^{\infty} functor will play a crucial role in the approach to the homotopy hypothesis that I will discuss.

    I’ll first define the category of cubical sets. Let □ ≤1\square_{\leq 1} be the unique category with the following properties.

    1) There are two objects, which I’ll denote by I 0I^{0} and I 1I^{1}.

    2) There is a pair of arrows as follows.

    3) There is an arrow as follows.

    4) The following diagrams in □ ≤1\square_{\leq 1} commute.

    I often refer to this category □ ≤1\square_{\leq 1} as the free-standing interval equipped with a contraction structure. This terminology comes from my thesis.

    We now denote by □\square the free strict monoidal category on □ ≤1\square_{\leq 1} in which I 0I^{0} is a unit object. A subtle but crucial point here: □\square is not the free strict monoidal category on □ ≤1\square_{\leq 1}. In the latter category, I 0I^{0} is not a unit object. One way to define □\square is to take the free strict monoidal category on □ ≤1\square_{\leq 1}, and then to identify the unit object with I 0I^{0}. I will make a lot of use, although not for a while, of the fact that being a ’free strict monoidal category with a designated unit’ is a 2-universal property, not only a 1-universal property.

    I’ll denote the object I 1⊗⋯⊗I 1I^{1} \otimes \cdots \otimes I^{1} of □\square, where the tensor product is taken nn times, by I nI^{n}.

    The category of cubical sets is the free co-completion of □\square. I’ll denote it by Set □ op\mathsf{Set}^{\square^{op}}, even though one of the foundational aspects of the work is that I will construct the free co-completion of a category in a purely categorical way, without relying upon a prior notion of set, and thus this notation will not really be appropriate. Another foundational aspect of the work is that I will work throughout with ’unbiased monoidal categories’, but I’ll ignore this aspect too for a good while.

    PS: Apologies for the missing commutative diagrams. I will edit once I have found a satisfactory way to include them. At the moment I am thinking of creating the diagrams in TikZ, and then including them somehow. Does anyone know if it is possible to include SVG code in a forum post? Or if there is some other good way to include images (if there is nothing better, I could host them on my own webpage).

    Edit: Commutative diagrams now added. They are png images, hosted at this bitbucket repository, together with the source code. I have used a little html to centre them.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeFeb 13th 2015
    • (edited Feb 13th 2015)

    You are very welcome to share material here on the forum. (The urge to put stuff on the nnLab is meant constructively: experience shows that material scattered through discussion forum threads is much harder to absorb later, than if the stabled bits of it have been compiled on a dedicated page. )

    Regarging diagrams: the nnLab at least supports SVG graphics, see at How to… include SVG figures. Other ways to include diagrams are discussed at How to… draw commutative diagrams (though the instructions there may need updating, not sure).

    • CommentRowNumber4.
    • CommentAuthorTim_Porter
    • CommentTimeFeb 13th 2015

    Richard: have you a personal n-Lab page (like my homepage). If you have why not develop a series of entries on this stuff using the richer environment there, and making it available when you want to for all to see. You can (I seem to remember) password protect some of the pages so need not fear spam. WHen it has satbilised then you can put it on the regular nLab pages.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 13th 2015

    Following on from the two comments above, you could always then advertise any additions as you make them in this discussion thread, while keeping the whole on an nLab page with its better graphics.

    • CommentRowNumber6.
    • CommentAuthorTim_Porter
    • CommentTimeFeb 13th 2015

    … that is what I was going to say next, so thanks David.

    Richard comments boxes on n-Lab pages are also a source of useful feedback, but then people have to tell others here where the comments boxes are.

    • CommentRowNumber7.
    • CommentAuthorKarol Szumiło
    • CommentTimeFeb 13th 2015

    A few versions of “cubical sets” can be found in the literature. Could you say which version your universal property describes? Are these plain cubical sets with standard face and degeneracy operators? Or do they include connections or perhaps something else?

  8. Urs, Tim, and David, thank you for your suggestions. I do not have a personal web page on the nLab, but for now I am quite keen to experiment with just posting in the nForum. As mentioned, my hope is to discuss the material with others, and a forum seems like the best place for that. The plan would be to collate the material after a while into something more stable: I certainly agree that leaving the material just in a forum discussion would not be best in the long term. If all goes to plan, I, every now and then, could make a ’summary post’, acting as a signpost through the discussion.

    I have settled on a way to include the diagrams that is sufficiently robust for me. In case anybody is interested: I write them in TikZ (I have some macros which mean that I can usually do this very quickly), and then export them to pdf files; convert them to png files (they could be converted to svg instead, but svg files tend not to display well on my browser); and then host them in a git repository, which I link to from the post. If anybody is interested, the source files can be found on the repository too.

    • CommentRowNumber9.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 13th 2015
    • (edited Feb 13th 2015)

    Karol, thank you for the question, it is exactly the kind of thing that I am looking for. Yes, the cubical sets that I have defined are the plain cubical sets that you refer to.

    However, connections will play a role later on, and indeed other structures as well.

    Connections (and other structures) could be included already at this stage, and taken into account in what I am about to do next. However, since we have less things to check when constructing functors canonically out of □\square than out of the version with connections, various things can be presented a little more simply when working with plain cubical sets, and thus I will do so.

    It is slightly surprising, but I have found that typically connections are not so important to build into cubical sets themselves: it is usuallly enough that they are present in the structures we build upon cubical sets (appropriate flavours of nn-groupoid, for example), or in the categories which we construct functors from cubical sets into (Top\mathsf{Top}, for example).

    Something that I have thought a few times about, though, is that it could be very nice to axiomatise the notion of a ’decorated category of cubes’ (i.e. a category of cubes with some extra structure: connections, etc), and to work in this generality. I certainly think that this should be possible, and that everything that I will do could be carried out in this generality.

    • CommentRowNumber10.
    • CommentAuthorRodMcGuire
    • CommentTimeFeb 13th 2015

    I do not have a personal web page on the nLab, but for now I am quite keen to experiment with just posting in the nForum.

    If you have lots of stuff you want to create in nLab like format you can always create a a bunch of pages in Doriath. To link from there to the actual nLab you have to give your links nLab: prefixes - e.g. [[nLab:modular lattice]]. If you use this prefix in the nLab or nForum it works fine but does show the namespace - modular lattice (nlab) which should be no big deal if you are copying and pasting to the nForum.

    • CommentRowNumber11.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 14th 2015
    • (edited Mar 16th 2015)

    (14th February 2015)

    Carrying on from #2, I’ll now define a functor as follows.

    The next step will be to use this functor to define the functor Ex ∞\mathsf{Ex}^{\infty} that we are aiming for.

    We’ll need a little notation when working with cubical sets.

    1) Given an integer n≥0n \geq 0, I’ll denote by □ n\square^{n} the cubical set represented by I nI^{n}. I often refer to □ n\square^{n} as the free-standing nn-cube.

    2) I’ll use the same notation for an arrow

    as for the corresponding arrow in □\square. Thus, for instance, there is a pair of arrows

    and an arrow as follows.

    3) Given a cubical set XX, we’ll refer to a morphism of cubical sets

    as an n-cube of XX.

    With this notation to hand, we will, to construct our functor Ex\mathsf{Ex}, fix a co-cartesian square as follows.

    In other words, we fix a pushout of the following diagram.

    The cubical set Sd ≤1(□ 1)\mathsf{Sd}_{\leq 1}(\square^{1}) can be pictured as follows.

    Indeed, we take two copies of □ 1\square^{1}

    and glue together the two 0-cubes depicted in blue. The arrow head points to the 0-cube corresponding to i 1i_{1}.

    • CommentRowNumber12.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 14th 2015
    • (edited Mar 16th 2015)

    We now define a functor

    as follows.

    1) To I 0I^{0}, we associate the cubical set □ 0\square^{0}.

    2) To I 1I^{1}, we associate the cubical set Sd ≤1(□ 1)\mathsf{Sd}_{\leq 1}(\square^{1}).

    3) To i 0i_{0}, we associate the following morphism of cubical sets.

    4) To i 1i_{1}, we associate the following morphism of cubical sets.

    5) To pp, we associate the canonical morphism

    of cubical sets such that the following diagram in Set □ op\mathsf{Set}^{\square^{op}} commutes.

    In fact, □ 0\square^{0} is a final object of Set □ op\mathsf{Set}^{\square^{op}}, so we could instead have made use of this universal property to define Sd ≤1(p)\mathsf{Sd}_{\leq 1}(p). I find the above definition to get more to the heart of the matter, though.

    Now, the monoidal structure on □\square gives rise to a (closed) monoidal structure on Set □ op\mathsf{Set}^{\square^{op}}: on representable presheaves, we specify that it agrees with the monoidal structure on □\square, and then we extend by colimits.

    By the universal property of □\square, the functor Sd ≤1\mathsf{Sd}_{\leq 1} gives rise to a functor as follows.

    In other words, we ’extend Sd ≤1\mathsf{Sd}_{\leq 1} monoidally’. For instance, Sd(□ 2)\mathsf{Sd}(\square^{2}) looks as follows.

    The squares here are not ’hollow’, they are 2-cubes. A pair of dots ••\bullet \bullet should be read as •⊗•\bullet \otimes \bullet. I have omitted the labels of the 1-cubes and 2-cubes.

    By the universal property of free co-completion, the functor

    extends to a functor

    which I’ll also denote by Sd\mathsf{Sd} (it agrees with our original Sd\mathsf{Sd} on representables).

    As is the case for any functor constructed in this way, Sd\mathsf{Sd} admits a right adjoint

    which is the functor Ex\mathsf{Ex} that we were aiming to construct in this post.

    The adjunction tells us that, given a cubical set XX, an nn-cube of Ex(X)\mathsf{Ex}(X) is a morphism as follows.

    For instance, a 11-cube of Ex(X)\mathsf{Ex}(X) consists of a pair of 11-cubes ff and gg of XX whose faces match up as follows.

  13. Thank you for your suggestion, Rod. Regarding the personal page in the nLab: this was in reply to Tim, I am not actually looking to create nLab-like pages. The ’experiment’ that I mentioned is with regard to posting mathematics in this way, with the hope of receiving questions and engaging in discussion, not really with regard to the presentation of the mathematics.

    As an aside to all, when I first made the last two posts, some of the figures did not display for a while. This was probably a temporary difficulty with connecting to bitbucket, or something like that, because they display fine now. Thus, if you do not see some of the figures, hold on for a little while, and they will hopefully appear eventually!

    • CommentRowNumber14.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 15th 2015
    • (edited Mar 16th 2015)

    (15th February 2015)

    Continuing from #12, I’ll now define a natural transformation as follows.

    This natural transformation will be used to define the Ex ∞\mathsf{Ex}^{\infty} functor that we are aiming to construct. To construct ι\iota, we will make use of the 2-universal property of □\square, and the 2-universal property of free co-completion. This technique is one of the innovations of our work on cubical homotopy theory, and we will see it again.

    Let

    be the canonical functor.

    Let

    denote the Yoneda embedding functor.

    Let

    be the restriction of the Yoneda embedding functor to □ ≤1\square_{\leq 1}, namely the composite functor y∘cany \circ \mathsf{can}.

    We begin by defining a natural transformation

    in the following way.

    1) To I 0I^{0}, we associate the following identity morphism.

    2) To I 1I^{1}, we associate the canonical morphism

    of cubical sets such that the following diagram in Set op\mathsf{Set}^{op} commutes.

    It is straightforward to check that the three diagrams which must commute do indeed commute.

    Recall that we can picture Sd ≤1(□ 1)\mathsf{Sd}_{\leq 1}(\square^{1}) as follows

    and that we can picture □ 1\square^{1} as follows.

    The morphism

    can then be pictured as sending the left 1-cube of Sd(□ 1)\mathsf{Sd}(\square^{1}) to the unique non-degenerate 1-cube of □ 1\square^{1}, whose faces are 00 and 11; and sending the right 1-cube of Sd(□ 1)\mathsf{Sd}(\square^{1}) to the degenerate 1-cube of □ 1\square^{1} whose faces are both 11.

    By the 2-universal property of □\square, the natural transformation

    gives rise to a natural transformation as follows.

    We now observe that it is the identity functor

    to which the Yoneda embedding functor

    gives rise by means of the universal property of Set □ op\mathsf{Set}^{\square^{op}} as a free co-completion.

    By means of the 2-universal property of Set □ op\mathsf{Set}^{\square^{op}} as a free co-completion, the natural transformation

    thus gives rise to a natural transformation as follows.

    I’ll again denote this natural transformation by ϕ\phi (it agrees with our earlier ϕ\phi on representables).

    • CommentRowNumber15.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 15th 2015
    • (edited Mar 16th 2015)

    Let

    be the unit natural transformation of the adjunction between Sd\mathsf{Sd} and Ex\mathsf{Ex}.

    Let Ex⋅ϕ\mathsf{Ex} \cdot \phi denote the natural transformation

    obtained by whiskering the following diagram.

    Let

    be the composition of natural transformations (Ex⋅ϕ)∘η(\mathsf{Ex} \cdot \phi) \circ \eta. In other words, the following triangle commutes.

    This natural transformation ι\iota is the one which we were aiming to define. Given a cubical set XX, it for instance sends a 1-cube

    of XX to the 1-cube of Ex(X)\mathsf{Ex}(X) pictured below, in which the right 1-cube is degenerate.

    • CommentRowNumber16.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 16th 2015
    • (edited Mar 16th 2015)

    (16th February 2015)

    Continuing from #15, I’ll in this post define the functor Ex ∞\mathsf{Ex}^{\infty} that we have been working towards.

    Actually, there is more than one possible definition. One possibility is to take the colimit of the following diagram in the category of functors from Set □ op\mathsf{Set}^{\square^{op}} to itself.

    Here ι⋅Ex n\iota \cdot \mathsf{Ex}^{n} for n≥1n \geq 1 is the whiskering of the following diagram.

    This is analogous to the definition of the well known Ex ∞\mathsf{Ex}^{\infty} functor in the simplicial case.

    However, one of the main points of departure of our work on the homotopy hypothesis will be to observe that, after 1-truncation, Ex ∞(X)\mathsf{Ex}^{\infty}(X), where XX is a cubical set, is very close to the underlying cubical set of the free groupoid on the 1-truncation of XX.

    There is a difference, however: the arrows of the free groupoid on the 1-truncation of XX can be viewed as zig-zags of nn arrows, where n≥0n \geq 0 is any even integer. Depicted below, for example, is a zig-zag consisting of six arrows.

    On the other hand, the 1-cubes of Ex ∞(X)\mathsf{Ex}^{\infty} (X) as defined at the beginning of this post can be viewed as zig-zags of 2 n2^{n} 1-cubes of XX, where n≥0n \geq 0 is an even integer. There is, for instance, no zig-zag of six 1-cubes of the same shape as in the previous picture.

    This difference is probably not essential for what I will do: I think it likely that one could adapt everything to go through for the Ex ∞\mathsf{Ex}^{\infty} functor defined above. However, it will be convenient for us to give a different definition, which makes the analogy between the 1-truncation of Ex ∞(X)\mathsf{Ex}^{\infty}(X) and the free groupoid on the 1-truncation of XX closer.

    The idea to use this alternative definition is due to Erik Rybakken. The key result that I will prove in future posts about this Ex ∞\mathsf{Ex}^{\infty} functor is joint work with Espen Auseth Nielsen and Erik Rybakken.

    Actually, whilst the analogy between Ex ∞(X)\mathsf{Ex}^{\infty}(X) and the free groupoid functor is something that has been an important part of my thinking about the homotopy hypothesis for quite a long time, it was not this which led Erik to his definition. It was rather to simplfy the construction of certain morphisms of cubical sets needed to carry out the proof of the ’key result’ mentioned in the previous paragraph.

    I’ll now work towards the definition of Ex ∞\mathsf{Ex}^{\infty} that we’ll adopt.

    Let us denote the functor

    by Sd ≤1 1\mathsf{Sd}_{\leq 1}^{1}, the morphism of cubical sets

    by r 0 1r_{0}^{1}, and the morphism of cubical sets

    by r 1 1r_{1}^{1}.

    We will now define inductively, for every integer n≥1n \geq 1, a functor as follows.

    Suppose that we have defined Sd ≤1 n\mathsf{Sd}_{\leq 1}^{n}, where n≥1n \geq 1 is an integer. We fix a co-cartesian square in Set □ op\mathsf{Set}^{\square^{op}} as follows.

    The functor Sd ≤1 n+1\mathsf{Sd}_{\leq 1}^{n+1} is then defined as follows.

    1) To I 0I^{0}, we associate the cubical set □ 0\square^{0}.

    2) To I 1I^{1}, we associate the cubical set Sd ≤1 n+1(□ 1)\mathsf{Sd}_{\leq 1}^{n+1}(\square^{1}).

    3) To i 0i_{0}, we associate the following morphism of cubical sets.

    4) To i 1i_{1}, we associate the following morphism of cubical sets.

    5) To pp, we associate the canonical morphism

    of cubical sets such that the following diagram in Set □ op\mathsf{Set}^{\square^{op}} commutes.

    • CommentRowNumber17.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 16th 2015
    • (edited Mar 16th 2015)

    In other words, to obtain Sd ≤1 n+1(□ 1)\mathsf{Sd}_{\leq 1}^{n+1}(\square^{1}), we glue a copy of Sd ≤1 1(□ 1)\mathsf{Sd}_{\leq 1}^{1}(\square^{1}) to the end of Sd ≤1 n(□ 1)\mathsf{Sd}_{\leq 1}^{n}(\square^{1}). For instance, Sd ≤1 3(□ 1)\mathsf{Sd}_{\leq 1}^{3}(\square^{1}) is obtained by glueing a copy of Sd ≤1 1(□ 1)\mathsf{Sd}_{\leq 1}^{1}(\square^{1})

    to the end of a copy of Sd ≤1 2(□ 1)\mathsf{Sd}_{\leq 1}^{2}(\square^{1}).

    This gives the following.

    By the universal property of □\square, the functor Sd ≤1 n\mathsf{Sd}_{\leq 1}^{n} gives rise to a functor as follows.

    By the universal property of free co-completion, this functor Sd n\mathsf{Sd}^{n} extends to a functor

    which I’ll also denote by Sd n\mathsf{Sd}_{n} (it agrees with Sd n\mathsf{Sd}^{n} on representables).

    As is the case for any functor constructed in this way, Sd n\mathsf{Sd}_{n} admits a right adjoint as follows.

    • CommentRowNumber18.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 16th 2015
    • (edited Mar 16th 2015)

    Let us denote the natural transformation

    by ϕ ≤1 1\phi_{\leq 1}^{1}, and denote the morphism of cubical sets

    by q 1q^{1}.

    Inductively, I’ll now define, for every integer n≥1n \geq 1, a natural transformation as follows.

    Suppose that we have defined ϕ ≤1 n\phi_{\leq 1}^{n}. We then define ϕ ≤1 n+1\phi_{\leq 1}^{n+1} in the following way.

    1) To I 0I^{0}, we associate the following identity morphism.

    2) To I 1I^{1}, we associate the canonical morphism

    of cubical sets such that the following diagram in Set op\mathsf{Set}^{op} commutes.

    It is straightforward to check that the three diagrams which must commute do indeed commute.

    Recall that we can picture Sd ≤1 3(□ 1)\mathsf{Sd}_{\leq 1}^{3}(\square^{1}) as follows

    and that we can picture Sd ≤1 2(□ 1)\mathsf{Sd}_{\leq 1}^{2}(\square^{1}) as follows.

    The morphism

    can be pictured as ’chopping off the last zig-zag’ of Sd ≤1 3(□ 1)\mathsf{Sd}_{\leq 1}^{3}(\square^{1}). Namely the first four 1-cubes, from the left, of Sd ≤1 3(□ 1)\mathsf{Sd}_{\leq 1}^{3}(\square^{1}) are sent to the corresponding four non-degenerate 1-cubes of Sd ≤1 2(□ 1)\mathsf{Sd}_{\leq 1}^{2}(\square^{1}); and the last two 1-cubes of Sd ≤1 3(□ 1)\mathsf{Sd}_{\leq 1}^{3}(\square^{1}) are both sent to the degenerate 1-cube whose faces are the rightmost 0-cube of Sd ≤1 2(□ 1)\mathsf{Sd}_{\leq 1}^{2}(\square^{1}).

    By the 2-universal property of □\square, the natural transformation

    gives rise to a natural transformation as follows.

    By means of the 2-universal property of Set □ op\mathsf{Set}^{\square^{op}} as a free co-completion, this natural transformation ϕ n+1\phi^{n+1} gives rise to a natural transformation as follows.

    • CommentRowNumber19.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 16th 2015
    • (edited Mar 16th 2015)

    Let us denote the natural transformation

    by ι 1\iota_{1}.

    For any integer n≥1n \geq 1, let

    be the unit natural transformation of the adjunction between Sd n+1\mathsf{Sd}_{n+1} and Ex n+1\mathsf{Ex}_{n+1}, and let

    be the co-unit natural transformation of the adjunction between Sd n\mathsf{Sd}_{n} and Ex n\mathsf{Ex}_{n}.

    Let η n+1⋅Ex n\eta_{n+1} \cdot \mathsf{Ex}_{n} denote the natural transformation

    obtained by whiskering the following diagram.

    Let Ex n+1⋅ϕ n+1⋅Ex n\mathsf{Ex}_{n+1} \cdot \phi_{n+1} \cdot \mathsf{Ex}_{n} denote the natural transformation

    obtained by whiskering the following diagram.

    Let Ex n+1⋅ε n\mathsf{Ex}_{n+1} \cdot \epsilon_{n} denote the natural transformation

    obtained by whiskering the following diagram.

    Let

    be the composition of these natural transformations. In other words, the following diagram commutes.

    Given a cubical set XX, the natural transformation ι 3\iota_{3} for instance sends a 1-cube

    of Ex 2(X)\mathsf{Ex}_{2}(X) to the 1-cube of Ex 3(X)\mathsf{Ex}_{3}(X) pictured below, in which the two 1-cubes in the rightmost zig-zag are degenerate.

    We define

    to be the colimit in the category of functors from Set □ op\mathsf{Set}^{\square^{op}} to Set □ op\mathsf{Set}^{\square^{op}} of the following diagram.

    Unwrapping this definition, a 11-cube, for instance, of Ex ∞(X)\mathsf{Ex}^{\infty}(X) can, as discussed earlier, be viewed as a zig-zag of 2n2n 1-cubes of XX, for some integer n≥0n \geq 0.

    • CommentRowNumber20.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 16th 2015
    • (edited Feb 16th 2015)

    My apologies to anyone who has already tried to read today’s post (split into four). I temporarily couldn’t see the pictures when previewing: some of the diagrams were out of order, and I had copied and pasted the wrong text towards the end. Everything has hopefully been tidied up now!

    • CommentRowNumber21.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 17th 2015
    • (edited Mar 16th 2015)

    (17th February 2015)

    Continuing from #19, we now have to hand a functor as follows.

    Two important points to keep in mind from the discussion so far are the following.

    1) This functor is not directly analogous to the simplicial Ex ∞\mathsf{Ex}^{\infty} functor, as discussed at the beginning of #16.

    2) We have not relied at any point on a presentation of □\square by generators and relations. Our functors and natural transformations have been constructed canonically.

    One of the properties of the simplicial Ex ∞\mathsf{Ex}^{\infty} functor is that the canonical morphism

    of simplicial sets is a weak equivalence. However, the only proof that I am aware of is very indirect, and relies upon the Milnor theorem that the adjunction morphism

    is a weak equivalence.

    The key property of the cubical Ex ∞\mathsf{Ex}^{\infty} functor that we have defined is analogous. To describe it, we need to prepare a little.

    Let 𝒜\mathcal{A} be a co-complete monoidal category, and let I=(I,i 0,i 1,p)\mathsf{I} = (I,i_{0},i_{1},p) be an interval in 𝒜\mathcal{A} equipped with a contraction structure, in the sense of my thesis. This structured interval determines (more precise details for everything in this introduction will be given later) a functor

    and thus a functor as follows.

    I will prove that, if the interval I\mathsf{I} admits certain further structures, then the arrow

    of 𝒜\mathcal{A} is a homotopy equivalence with respect to I\mathsf{I}, where

    the canonical natural transformation.

    The principal points that I wish to draw attention to are the following.

    1) Taking 𝒜\mathcal{A} to be Top\mathsf{Top}, and taking I\mathsf{I} to be the usual topological interval, our result gives that

    is a weak equivalence of cubical sets. The extra generality of our result places our proof in a conceptual framework, but is important not only for this aesthetic reason. We will actually make use of a different choice of 𝒜\mathcal{A} when working on the homotopy hypothesis.

    2) Our proof is completely different from the proof in the simplicial setting referred to earlier. In particular, it is constructive. We will construct by hand a homotopy inverse to

    and by hand the homotopy that we need to show that we have a homotopy equivalence.

    At this point, having completed the construction of the cubical Ex ∞\mathsf{Ex}^{\infty} functor, I was originally planning to assume a few properties of our functor Ex ∞\mathsf{Ex}^{\infty}, and a few other things, and begin discussing the homotopy hypothesis directly. However, I am fond of our approach to the result described above, and have decided to give the details now, before moving onto the homotopy hypothesis. As mentioned in a previous post, all work on this result is joint with Espen Auseth Nielsen and Erik Rybakken.

    I have intended since our work on this result began to take shape to dedicate it to the memory of Daniel Kan. I never met or corresponded with him, but the tools and ideas that he introduced in his work are used in almost every line that I write, and have had a great influence on my mathematical thought. Category theory was very young when he wrote his first papers, and it is remarkable to me that he was already able to make use of the language, and to make crucial developments in it, to lay the foundations for abstract homotopy theory. His influence is of course widely acknowledged, but my impression nevertheless is that its extent is still to be fully appreciated: I think that future historians of mathematics will come to see his early work as highly significant, the sapling from which the vast tree of abstract homotopy theory grew.

    • CommentRowNumber22.
    • CommentAuthorKarol Szumiło
    • CommentTimeFeb 17th 2015

    Richard, thank you for a very thorough presentation of your results. I wish more people did this.

    Are you aware of the paper Simplicial Sets from Categories by Latch, Thomason and Wilson? The proof of their Theorem 4.1 can be easily adapted to a neat proof that X→ExXX \to \Ex X is a weak equivalence for every simplicial set XX. The argument can be presented in a completely combinatorial way without any reference to topological spaces whatsoever. I think that this approach should work over an elegant Reedy category (is □\square such?) provided that a reasonable Ex\Ex functor can be constructed (I haven’t digested your definition yet so I don’t know whether it is in line with that argument).

    • CommentRowNumber23.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 17th 2015

    I know of two other “purely combinatorial” proofs that X→Ex ∞(X)X \to Ex^\infty (X) is a weak homotopy homotopy equivalence of simplicial sets:

    1. Proposition 2.3.19 in [Cisinski, Les préfaisceaux comme modèles des types d’homotopie], which mainly relies on the fact that diag:ssSet→sSetdiag : \mathbf{ssSet} \to \mathbf{sSet} takes degreewise weak homotopy equivalences to weak homotopy equivalences. It seems to be closely related to the theorem of Latch, Thomason, and Wilson that Karol mentioned.

    2. A colleague of mine has recently given an explicit presentation of X→Ex ∞(X)X \to Ex^\infty (X) as an anodyne extension (indeed, as a relative cell complex built from horn inclusions). Of course, this depends very much on the combinatorics of simplices, but it does eventually give an independent construction of the model structure on simplicial sets.

    • CommentRowNumber24.
    • CommentAuthorKarol Szumiło
    • CommentTimeFeb 17th 2015

    As far as I can tell Cisinski’s proof is basically the same as that of LTW. The thing is that all the prerequisites for that argument (preservation of weak equivalences by the diagonal functor being the crucial one) can be established in an elementary way without going through the abstract theory of model structures on categories of presheaves.

    When it comes to the second approach, of course it follows a posteriori that the map X→Ex ∞XX \to \Ex^\infty X is an anodyne extension, but I always assumed that writing that down explicitly would be a hopelessly tedious task. Can you say anything about that? In particular does it work for Ex\Ex or only Ex ∞\Ex^\infty?

    • CommentRowNumber25.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 18th 2015
    • (edited Feb 18th 2015)

    Thank you for the encouragement, Karol!

    Thank you very much to you both for the interesting comments. Please jump in with references as you have done here whenever you wish!

    I was aware of both the paper of Latch, Thomason and Wilson and the work of Cisinski, but had forgotten about these proofs! It is great that you have reminded me.

    I think that this approach should work over an elegant Reedy category (is □\square such?)

    I had not thought much about this before, but, yes, it seems to me that □\square is an elegant Reedy category. That it is a Reedy category is well known: a reference for the third property in the definition of a Reedy category given in the nLab is Lemma 4.1 in the paper Cubical sets and their site of Grandis and Mauri, but the result for example also appears as Lemme 8.4.4 in the work Les préfaisceaux comme modèles des types d’homotopie of Cisinski, and probably has been known for much longer. Given the usual presentation of □\square by generators and relations, it is straightforward to see how a proof should go, appealing to the functoriality of −⊗−- \otimes -, although writing down a truly rigorous proof might take some care.

    I have not found a reference which observes that □\square is an elegant Reedy category, but I think this should follow from Proposition 1.2.1 in Notes on simplicial homotopy theory by Joyal and Tierney, which is one way to prove it for Δ\Delta. I haven’t checked all the details carefully, though.

    If I read Theorem 5.1 in the paper of Grandis and Mauri correctly, it would seem to me that the category of cubes with connections can also be viewed as a Reedy category, if we regard both co-degeneracies and co-connections as belonging to R −R_{-}. However, this doesn’t seem particularly natural to me. The result of Grandis and Mauri would rather suggest considering factorisations into three kinds of maps, not only two. I’ve not thought about whether the category of cubes with connections, if able to be viewed as a Reedy category in this way, is elegant, but it seems possible.

    I think that this approach should work over an elegant Reedy category provided that a reasonable Ex functor can be constructed

    That would be interesting! More generally, it would be very interesting to see any kind of serious work along these lines in abstract homotopy theory, namely working in an axiomatic framework that captures both simplicial and cubical sets. Of course there is the notion of a test category, but this seems to me to be too general. The notion of a Reedy category is closer, but still does not feel right to me. One reason is given above, but, more conceptually, it doesn’t seem to me the existence/uniqueness of the factorisations required in the definition of a Reedy category is at the heart of why Δ\Delta and □\square are good categories of shapes for abstract homotopy theory. I have never used this when working with cubical sets, for instance.

    My feeling is that the category of cubes is somehow ’universal’ amongst categories of shapes for abstract homotopy theory. It would be interesting, taking this idea seriously, to try to formally develop the homotopy theory of simplicial sets ’from a cubical point of view’. A point of view that is a little similar to this can be found in Jardine’s two papers on cubical homotopy theory: Cubical homotopy theory - a beginning and Categorical homotopy theory. The question of formalising the notion of a ’decorated category of cubes’ that I mentioned in #9 is closely related.

    The proof that I will give is of a very different flavour from that of Latch, Thomason, and Wilson, and that of Cisinski. Perhaps one could summarise the difference by saying that the proof I will give is ’structural’ rather than ’combinatorial’. But this will become clearer when I’ve given further details.

    • CommentRowNumber26.
    • CommentAuthorKarol Szumiło
    • CommentTimeFeb 18th 2015
    • (edited Feb 18th 2015)

    My feeling is that the category of cubes is somehow ’universal’ amongst categories of shapes for abstract homotopy theory.

    Personally, I feel that this distinction should go to Δ\Delta but that’s just based on my own astonishment at how neat and elegant simplicial homotopy theory is. If I try to think about it in an unbiased way I don’t see any clear advantages of either approach. In both cases we start with some basic notion of a 11-dimensional homotopy and we follow some pattern of generating notions of homotopies of higher dimensions, both look equally ad hoc to me. I see where you are coming from with the universal property of □\square but the choice of a monoidal category as the basic structure seems just as arbitrary as the choice of a Reedy category.

    That would be interesting! More generally, it would be very interesting to see any kind of serious work along these lines in abstract homotopy theory, namely working in an axiomatic framework that captures both simplicial and cubical sets.

    In one of his papers Clemens Berger mentions a notion of a “geometric Reedy category” that he tried to develop together with Cisinski that was supposed to do something like that. I asked him about it and from what he told me it seemed that the project didn’t get too far and that their ideas weren’t particularly compatible with the subdivision/Ex\Ex approach. This is a problem that I occasionally ponder idly but somehow it never takes off…

    • CommentRowNumber27.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 20th 2015
    • (edited Feb 20th 2015)

    Personally, I feel that this distinction should go to Δ\Delta but that’s just based on my own astonishment at how neat and elegant simplicial homotopy theory is.

    I hope to eventually convince people reading that cubical homotopy theory is just as neat and elegant! Indeed, I would even argue that cubical homotopy is still more elegant, because there is an extra level of structure which one can make use of to construct cubical sets and morphisms between them canonically, rather than writing out explicit formulae and checking that relations hold. I should say, though, that one can certainly work in this way with cubical sets too.

    In particular, I find that working cubically allows one to formally ’figure things out in low dimensions (where one can draw pictures), and then abstract from this to all dimensions’, which of course is how one works in practise in simplicial homotopy theory (or, perhaps, I should say, ’foundational simplicial homotopy theory’, namely before one has developed enough tools to be able to work with a ’higher level language’).

    If I try to think about it in an unbiased way I don’t see any clear advantages of either approach. In both cases we start with some basic notion of a 1-dimensional homotopy and we follow some pattern of generating notions of homotopies of higher dimensions, both look equally ad hoc to me. I see where you are coming from with the universal property of □\square but the choice of a monoidal category as the basic structure seems just as arbitrary as the choice of a Reedy category.

    I agree that what you write in the second sentence is the heart of the matter. I personally do find the data of an interval and a monoidal structure to be more natural than the notion of a Reedy category for capturing this idea, though. Having an interval and a monoidal structure is a direct abstraction from Top\mathsf{Top}, once one notices that the fact that the monoidal structure in Top\mathsf{Top} is cartesian is not necessary for the development of homotopy theory: we just need certain structures to exist and to interact well with the monoidal structure. In particular, we will have a functor out of our category of shapes whenever we have an appropriate interval in some other monoidal category, which I feel to be very significant: I don’t see the structure of a Reedy category as giving us the possibility to construct functors out of it.

    But I do not have any precise way to formulate the sense in which I feel that the category of cubes should be considered ’universal’ amongst categories of shapes, so can only give ’philosophical’ arguments such as these!

    This is a problem that I occasionally ponder idly but somehow it never takes off…

    Thanks for mentioning this! I would certainly be very interested in developing an abstract notion of ’category of shape’, and it is definitely something that I would like to think about in the future. If I do so, I’ll let you know!

    • CommentRowNumber28.
    • CommentAuthorKarol Szumiło
    • CommentTimeFeb 20th 2015

    Having an interval and a monoidal structure is a direct abstraction from Top\mathsf{Top}, once one notices that the fact that the monoidal structure in Top\mathsf{Top} is cartesian is not necessary for the development of homotopy theory: we just need certain structures to exist and to interact well with the monoidal structure.

    Again, the choice of the monoidal structure of Top\mathsf{Top} as the starting point is arbitrary. I could equally well generate higher homotopies by using factorizations in Top\mathsf{Top} which would lead to me to a Reedy type structure. However, I think that it will be more productive to let you go on with your story rather than do a full on rebuttal. I’m looking forward to the continuation of your write up.

    • CommentRowNumber29.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 20th 2015
    • (edited Feb 20th 2015)

    Again, the choice of the monoidal structure of Top as the starting point is arbitrary.

    Yes, I would agree with that. When looking for an axiomatic framework, one of course has to start somewhere, in a way which is going to be a matter of taste and efficacy (whether it will lead to a good theory). I personally find developing homotopy theory in the setting of structured intervals/cylinders/co-cylinders together with a monoidal structure very satisfactory, but certainly what I wrote about finding the monoidal structure of the category of cubes more natural than its Reedy structure is a consequence of, or at least very closely tied to, this point of view. I agree entirely that one may well be able to make a convincing argument for a different point of view.

    Maybe a better illustration of the difference I see between the monoidal and Reedy settings is that everything in the monoidal setting is built up from a handful of objects and arrows that are part of the structure, whereas in the Reedy setting one needs to know something about all arrows as part of the structure (this is also the case with the cylindrical approach to abstract homotopy theory of Kamps, which relies upon ’Kan-like conditions’). But I completely agree that there will not be an absolute reason why the one should be considered preferable over the other: one will only be able to give justifications that take certain things as common ground.

    I’m looking forward to the continuation of your write up.

    Thank you! My apologies for the delay, a few things cropped up, but I have nearly finished preparing the next posts now. I’m not quite sure when I’ll get the chance to put the finishing touches, but at the latest it should be early next week.

    • CommentRowNumber30.
    • CommentAuthorUlrik
    • CommentTimeFeb 21st 2015

    I would just like to add that I’m enjoying reading the installments of this mathematical serial. I’m also particularly interested to hear your thoughts, Richard, on the choice of the monoidal rather than the cartesian cube category on an interval. It seems to me that the latter has many advantages as well.

    • CommentRowNumber31.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 24th 2015
    • (edited Feb 24th 2015)

    Thank you for the encouragement, Ulrik!

    It is taking a bit longer than expected to finish off the next post, because I will go a little further in that post than originally planned, but it’ll be ready soon.

    I’m also particularly interested to hear your thoughts, Richard, on the choice of the monoidal rather than the cartesian cube category on an interval. It seems to me that the latter has many advantages as well.

    Thank you for the interesting question! In short, I agree with you!

    On the one hand, the free cartesian category on □ ≤1\square_{\leq 1} with unit I 0I^{0}, let us denote it by □ cart\square^{\mathsf{cart}} is a ’decorated category of cubes’ (i.e. similar to □\square but with extra structure). From this point of view, the same remarks apply as in #9: it is harder to construct functors out of it than out of □\square. However, this does not matter, because □ cart\square^{\mathsf{cart}} has its own universal property, which makes it just as easy to construct functors out of it.

    Moreover, cubical homotopy theory with respect to this category would seem to me to be very well suited to constructing models of type theories. The cartesian monoidal structure on Set (□ cart) op\mathsf{Set}^{(\square^{\mathsf{cart}})^{op}} would have the same nice conceptual properties as the non-cartesian monoidal structure on cubical sets, that I was advocating the use of for constructing models of type theory in this discussion, but would also allow one to model type theory in the usual way which one can with a cartesian monoidal structure.

    At the moment, I also see no reason why the work I am outlining on the homotopy hypothesis would not go through for this category. It is crucial that the monoidal structure we work with is ’topological’, namely the tensor product of an mm-cube and an nn-cube is an (m+n)(m+n)-cube, but this would be the case for presheaves on □ cart\square^{\mathsf{cart}}.

    Indeed the only advantage that I can see of □\square over □ cart\square^{\mathsf{cart}} is the obvious one that it interacts well with more general categories (this is just the difference in generality between an arbitrary monoidal structure and a cartesian one).

    It is interesting to ponder how □ cart\square^{\mathsf{cart}} would fit into a formalism for describing ’shape categories’ appropriate for homotopy theory, that Karol and I have been discussing. It may for instance be that, rather than consider just ’decorated categories of cubes’, one should consider more general ’decorated free structures’ on □ ≤1\square_{\leq 1}. Maybe one can even work with quite general 2-monads on Cat\mathsf{Cat}, rather than just those describing monoidal-ness or cartesian-ness. I have not thought about this at all, but it is something to keep in mind!

    • CommentRowNumber32.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    (Completed on the 2nd of March, but posted on the 9th of March, as the nForum was down from earlier on the 2nd until some time on the 8th. This post will be spread over a large number of entries).

    Continuing from #21, I’ll now begin working towards the proof of the result mentioned in that post.

    Let us denote by α\alpha the natural transformation

    which is part of the data of the colimit defining Ex ∞\mathsf{Ex}^{\infty}.

    Let 𝒜\mathcal{A} be a co-complete monoidal category, and let I̲=(I,i 0 𝒜,i 1 𝒜,p 𝒜)\underline{\mathsf{I}} = (\mathsf{I},i^{\mathcal{A}}_{0},i^{\mathcal{A}}_{1},p^{\mathcal{A}}) be an interval in 𝒜\mathcal{A} equipped with a contraction structure, in the sense of VI of my thesis. The following defines a functor

    which I’ll denote by |−| ≤1\left| - \right|_{\leq 1}.

    1) To I 0I^{0}, we associate the unit object 11 of the monoidal structure of 𝒜\mathcal{A}.

    2) To I 1I^{1}, we associate the object I\mathsf{I} of 𝒜\mathcal{A}.

    3) To the arrows i 0i_{0}, i 1i_{1}, and pp of □ ≤1\square_{\leq 1}, we associate the arrows i 0 𝒜i_{0}^{\mathcal{A}}, i 1 𝒜i_{1}^{\mathcal{A}}, and p 𝒜p^{\mathcal{A}} of 𝒜\mathcal{A} respectively.

    By means of the universal property of □\square, the functor

    gives rise to a functor as follows.

    By means of the universal property of Set □ op\mathsf{Set}^{\square^{op}} as a free co-completion, the functor |−| □\left| - \right|_{\square} gives rise to a functor as follows.

    • CommentRowNumber33.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Before constructing the natural transformations ρ n\rho_{n}, let us first explore the idea. Of greatest significance is the idea behind the definition of the natural transformation

    at the level of 1-cubes, which is as follows. Given a cubical set XX, recall that a 1-cube zz of Ex 1(X)\mathsf{Ex}_{1}(X) is a zig-zag of 1-cubes of XX as shown below.

    We wish to send zz to the 1-cube of S(|X|)S\big( \left| X \right| \big) corresponding to the path in |X|\left| X \right| given by g −1⋅fg^{-1} \cdot f. In other words, we reverse the path in |X|\left| X \right| corresponding to gg, and then glue it to the end of the path in |X|\left| X \right| corresponding to ff. The involution structure precisely allows us to ’reverse’ paths, and the subdivision structure precisely allows us to ’glue’ them.

    It is not clear to me whether it is possible to modify □\square in order to be able to work with XX instead of S(|X|)S\big( \left| X \right| \big). We could require that cubical sets have involutions, which would allow to reverse 1-cubes in XX, but to build a subdivision structure into an interval, one would have to do so as an absolute pushout, which seems tricky. In any case, it would take quite a lot of work to construct functors out of such a modified □\square.

    One of the main technical ideas in the proof I will give is that there is no need for such a modification of □\square: to ’replace XX by S(|X|)S\big( \left| X \right| \big)’ allows us to make sense of ’reversing and glueing’ 1-cubes (and indeed nn-cubes for any nn). More generally, this replacement ’makes any structures in 𝒜\mathcal{A} available inside Set □ op\mathsf{Set}^{\square^{op}}’. This is one aspect of what I was getting at in the fourth paragraph of my reply to Karol in #9.

    The simple idea for the definition of ρ 1\rho_{1} at the level of 1-cubes described above does not quite work when we do not have strictness of right identities. Indeed, the obvious natural transformation

    to choose for ρ 0\rho_{0} is the unit natural transformation coming from the adjunction between SS and |−|\left| - \right|. However, the diagram

    does not then necessarily commute. To see this, let

    be a 1-cube of XX. Taking the longer route through the triangle

    gives, noting that the reverse of a constant path is constant since the involution structure v 𝒜v^{\mathcal{A}} is compatible with p 𝒜p^{\mathcal{A}}, the path c x 1⋅fc_{x_{1}} \cdot f, namely the constant path at x 1x_{1} glued to the end of ff. Since we do not necessarily have strictness of right identities, this path is not necessarily ff on the nose, whilst ff is the path that we obtain by taking the shorter route through the triangle.

    • CommentRowNumber34.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Let us now discuss how we can get around this difficulty. We will now assume that our subdivision structure is compatible with p 𝒜p^{\mathcal{A}}, in the sense of VI of my thesis. This condition is much weaker than strictness of right identities: it says that the glueing together two constant paths gives a constant path. This of course holds for the interval in Top\mathsf{Top}.

    We tweak ρ 0\rho_{0} as follows: we send a 1-cube

    of XX to the 1-cube of S(|X|)S\big( \left| X \right| \big) corresponding to the path c x 1⋅fc_{x_{1}} \cdot f in |X|\left| X \right|.

    We then tweak ρ 1\rho_{1} as follows: we send a 1-cube of Ex 1(X)\mathsf{Ex}_{1}(X), namely a zig-zag

    of 1-cubes of XX, to the 1-cube of S(|X|)S\big( \left| X \right| \big) corresponding to the path (c x 2⋅g −1)⋅f(c_{x_{2}} \cdot g^{ -1}) \cdot f in |X|\left| X \right|.

    We then tweak ρ 2\rho_{2} as follows: we send a 1-cube of Ex 2(X)\mathsf{Ex}_{2}(X), namely a zig-zag

    of 1-cubes of XX, to the 1-cube of S(|X|)S\big( \left| X \right| \big) corresponding to the path ((c x 4⋅(g 2 −1⋅f 2))⋅g 1 −1)⋅f 1\Big( \big( c_{x_{4}} \cdot (g_{2}^{-1} \cdot f_{2} ) \big) \cdot g_{1}^{-1} \Big) \cdot f_{1} in |X|\left| X \right|.

    We then tweak ρ 3\rho_{3} as follows: we send a 1-cube of Ex 3(X)\mathsf{Ex}_{3}(X), namely a zig-zag

    of 1-cubes of XX, to the 1-cube of S(|X|)S\big( \left| X \right| \big) corresponding to the path (((c x 6⋅(g 3 −1⋅f 3))⋅(g 2 −1⋅f 2))⋅g 1 −1)⋅f 1\bigg( \Big( \big( c_{x_{6}} \cdot (g_{3}^{-1} \cdot f_{3}) \big) \cdot \big( g_{2}^{-1} \cdot f_{2} \big) \Big) \cdot g_{1}^{-1} \bigg) \cdot f_{1} in |X|\left| X \right|.

    We then tweak ρ n\rho_{n} for every n≥4n \geq 4 in a similar way: we send a 1-cube of Ex n(X)\mathsf{Ex}_{n}(X), namely a zig-zag

    of 2n2n 1-cubes of XX, to the path constructed in the same way as the path to which the zig-zag obtained by ’chopping off’ f nf_{n} and g ng_{n} is sent under ρ n−1(X)\rho_{n-1}(X), except that the constant path c x 2(n−1)c_{x_{2(n-1)}} is replaced by a bracket with c x 2n⋅(g n −1⋅f n)c_{x_{2n}} \cdot (g_{n}^{-1} \cdot f_{n}) inside.

    It is crucial to get the bracketing in the paths we have just described right, since (think again of Top\mathsf{Top}) glueing of paths is not in general associative on the nose.

    • CommentRowNumber35.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    There is a different possibility for getting around the lack of strictness of identities. Instead of working with Ex ∞\mathsf{Ex}^{\infty}, we could work with the homotopy colimit of the diagram used to define Ex ∞\mathsf{Ex}^{\infty}, namely the homotopy colimit of the following diagram.

    By ’homotopy colimit’ here, I mean that we take the (ordinary!) colimit of the modification of the diagram above in which we ’insert a cylinder’ at every step: we replace the natural transformation

    by the following diagram of natural transformations

    and replace the natural transformation

    for every n≥1n \geq 1 by the following diagram of natural transformations.

    Let us denote the homotopy colimit, in this sense, of the diagram

    by Ex h ∞\mathsf{Ex}^{\infty}_{h}.

    Assuming that I̲\underline{\mathsf{I}} is equipped with what Grandis terms a ’zero collapse structure’ in the paper Categorically algebraic foundations for homotopical algebra, which gives a means to construct a homotopy between c x 1⋅fc_{x_{1}} \cdot f and ff for a 1-cube

    of XX, we will be able to construct a map from Ex h ∞(X)\mathsf{Ex}_{h}^{\infty}(X) to S(|X|)S\big( \left| X \right| \big).

    For every cubical set XX, I believe it possible to demonstrate that

    is a cofibration, in the sense of VIII of my thesis, if I̲\underline{\mathsf{I}} is equipped with a certain structure, and, given this same structure, that

    is a cofibration.

    It should then follow that

    is a homotopy equivalence for any cubical set XX, where

    is the canonical morphism of cubical sets.

    However, I will not follow this approach. Instead, I follow the simpler ’tweaking’ method that I described first: I wish to give as ’down to earth’ a proof as possible, which can hopefully give people a clear understanding of why we should expect

    to be a homotopy equivalence for any cubical set XX.

    • CommentRowNumber36.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Let us now embark upon the formal construction of the natural transformations ρ n\rho_{n}. As mentioned, we now assume that I̲\underline{\mathsf{I}} is equipped with an involution structure v 𝒜v^{\mathcal{A}} compatible with p 𝒜p^{\mathcal{A}}, and a subdivision structure (S,r 0 𝒜,r 1 𝒜,s 𝒜)(\mathsf{S},r^{\mathcal{A}}_{0},r^{\mathcal{A}}_{1},s^{\mathcal{A}}) compatible with p 𝒜p^{\mathcal{A}}, in the sense of VI of my thesis.

    Let us first work towards defining ρ 0\rho_{0}.

    Let us denote by

    the canonical arrow of 𝒜\mathcal{A} such that the following diagram in 𝒜\mathcal{A} commutes.

    We define a natural transformation

    in the following way.

    1) To the object I 0I^{0}, we associate the following identity arrow.

    2) To the object I 1I^{1}, we associate the arrow

    of 𝒜\mathcal{A}.

    It is straightforward to check that the three diagrams that must commute do indeed commute (for the diagram involving p 𝒜p^{\mathcal{A}}, we appeal to our assumption that the subdivision structure (S,r 0 𝒜,r 1 𝒜,s 𝒜)(\mathsf{S},r_{0}^{\mathcal{A}},r_{1}^{\mathcal{A}},s^{\mathcal{A}}) is compatible with p 𝒜p^{\mathcal{A}}).

    By means of the 2-universal property of □\square, the natural transformation τ 0 ≤1\tau_{0}^{\leq 1} gives rise to a natural transformation as follows.

    By means of the 2-universal property of free co-completion, the natural transformation τ 0 □\tau_{0}^{\square} gives rise to a natural transformation as follows.

    Let us denote by η 𝒜\eta_{\mathcal{A}} the unit natural transformation

    of the adjunction between SS and |−|\left| - \right|.

    We define ρ 0\rho_{0} to be the natural transformation (S⋅τ 0)∘η 𝒜(S \cdot \tau_{0}) \circ \eta_{\mathcal{A}}. In other words, the following diagram commutes.

    Here S⋅τ 0S \cdot \tau_{0} is the natural transformation obtained by whiskering the following diagram.

    • CommentRowNumber37.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Let us now work towards defining ρ 1\rho_{1}. I will for the time being use the original notation Ex\mathsf{Ex} and Sd\mathsf{Sd} instead of Ex 1\mathsf{Ex}_{1} and Sd 1\mathsf{Sd}_{1}, and the same in similar cases. When we come to work towards defining ρ n\rho_{n} for n≥2n \geq 2, we’ll return to the notation Ex n\mathsf{Ex}_{n} and Sd n\mathsf{Sd}_{n}.

    Let us denote by

    the canonical arrow of 𝒜\mathcal{A} such that the following diagram in 𝒜\mathcal{A} commutes.

    Let us denote by

    the canonical arrow of 𝒜\mathcal{A} such that the following diagram in 𝒜\mathcal{A} commutes.

    We define a natural transformation

    in the following way.

    1) To the object I 0I^{0}, we associate the following identity arrow.

    2) To the object I 1I^{1}, we associate the arrow

    of 𝒜\mathcal{A}.

    It is straightforward to check that the three diagrams that must commute do indeed commute (for the diagram involving pp, we appeal to both our assumption that the subdivision structure (S,r 0 𝒜,r 1 𝒜,s 𝒜)(\mathsf{S},r_{0}^{\mathcal{A}},r_{1}^{\mathcal{A}},s^{\mathcal{A}}) is compatible with p 𝒜p^{\mathcal{A}} and that the involution structure v 𝒜v^{\mathcal{A}} is compatible with p 𝒜p^{\mathcal{A}}).

    Noting that it is the functor

    to which the functor |Sd ≤1(−)|\left| \mathsf{Sd}_{\leq 1}(-) \right| gives rise by means of the universal property of □\square, the natural transformation τ 1 ≤1\tau_{1}^{\leq 1} gives rise, by means of the 2-universal property of □\square, to a natural transformation as follows.

    Noting that it is the functor

    to which the functor

    gives rise by means of the universal property of free co-completion, the natural transformation τ 1 □\tau_{1}^{\square} gives rise, by means of the 2-universal property of free co-completion, to a natural transformation as follows.

    • CommentRowNumber38.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Let us denote by ε 𝒜\epsilon_{\mathcal{A}} the co-unit natural transformation

    of the adjunction between SS and |−|\left| - \right|.

    Let us denote by ε\epsilon the co-unit natural transformation

    of the adjunction between Sd\mathsf{Sd} and Ex\mathsf{Ex}.

    Let us denote by τ 1 adj\tau_{1}^{\mathsf{adj}} the natural transformation

    given by the composition of four natural transformations on the longer route around the following triangle.

    In other words, this triangle commutes.

    Here η 𝒜⋅(Ex∘S)\eta_{\mathcal{A}} \cdot (\mathsf{Ex} \circ S) is the natural transformation obtained by whiskering the following diagram.

    The natural transformation S⋅τ 1⋅(Ex∘S)S \cdot \tau_{1} \cdot (\mathsf{Ex} \circ S) is that obtained by whiskering the following diagram.

    The natural transformation (S∘|−|)⋅ε⋅S(S \circ \left| - \right|) \cdot \epsilon \cdot S is that obtained by whiskering the following diagram.

    The natural transformation S⋅ε 𝒜S \cdot \epsilon_{\mathcal{A}} is that obtained by whiskering the following diagram.

    This construction of τ 1 adj\tau_{1}^{\mathsf{adj}} given τ 1\tau_{1} is the canonical procedure for obtaining a natural transformation between right adjoints given a natural transformation between left adjoints, noting that ε 𝒜)∘(|−|)⋅ε⋅S)\epsilon_{\mathcal{A}}) \circ \big( \left| - \right|) \cdot \epsilon \cdot S \big) is the co-unit for the adjunction between |Sd|\left| \mathsf{Sd} \right| and Ex∘S\mathsf{Ex} \circ S.

    We define

    to be the natural transformation given by (τ 1 adj⋅|−|)∘(Ex⋅η 𝒜)(\tau_{1}^{\mathsf{adj}} \cdot \left| - \right|) \circ (\mathsf{Ex} \cdot \eta_{\mathcal{A}}). In other words, the following diagram commutes.

    Here η 𝒜⋅Ex\eta_{\mathcal{A}} \cdot \mathsf{Ex} is the natural transformation obtained by whiskering the following diagram.

    The natural transformation τ 1 adj⋅|−|\tau_{1}^{\mathsf{adj}} \cdot \left| - \right| is obtained by whiskering the following diagram.

    • CommentRowNumber39.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    Having now defined ρ 0\rho_{0} and ρ 1\rho_{1}, let us prove that the diagram

    commutes.

    The heart of the matter is to demonstrate that the following diagram commutes.

    We proceed as follows.

    1) The following diagram commutes.

    2) The following diagram commutes.

    That the triangle

    commutes holds by our assumption that v 𝒜v^{\mathcal{A}} is compatible with p 𝒜p^{\mathcal{A}}.

    3) By 1) and 2), the following diagram commutes.

    4) Let

    be the natural transformation of VI.18 in my thesis, with respect to (S,r 0 𝒜,r 1 𝒜,s 𝒜)(\mathsf{S}, r_{0}^{\mathcal{A}}, r_{1}^{\mathcal{A}}, s^{\mathcal{A}}) and p 𝒜p^{\mathcal{A}}. By definition, the following diagram commutes.

    Hence the following diagram commutes.

    5) By the universal property of a co-cartesian square, we deduce from 3) and 4) that the following diagram commutes.

    6) By our assumption that (S,r 0 𝒜,r 1 𝒜,s 𝒜)(\mathsf{S}, r_{0}^{\mathcal{A}}, r_{1}^{\mathcal{A}}, s^{\mathcal{A}}) is compatible with p 𝒜p^{\mathcal{A}}, the following diagram commutes.

    7) We deduce from 5) and 6) that the following diagram commutes.

    8) We deduce from 7) and the definition of the arrow oo that the following diagram commutes.

    9) By definition of oo and qq, the following diagram commutes.

    10) By 8) and 9), the following diagram commutes.

    11) By definition of q rq_{r}, the following diagram commutes.

    12) By the universal property of a co-cartesian square, we deduce from 10) and 11) that the following diagram commutes.

    13) We deduce from 12) that the following diagram commutes.

    In other words, the following diagram commutes.

    • CommentRowNumber40.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    14) In addition, the following diagram commutes.

    15) We conclude from 13) and 14) that the following diagram commutes.

    16) Noting that it is the natural transformation

    to which the natural transformation

    gives rise by means of the 2-universal property of □\square and the 2-universal property of free co-completion, we conclude from 15) that the following diagram commutes, as we wished to show.

    The remainder of our proof that the diagram

    commutes will be a reduction to the diagram

    whose commutativity we have just established.

    To carry out this reduction, we will need a few observations which hold in an arbitrary strict 2-category 𝒞\mathcal{C}.

    1) Let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 2-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    Let us demonstrate this. By definition, ζ 1∘ζ 0\zeta_{1} \circ \zeta_{0} is obtained by pasting the 2-arrows in the following diagram. I have omitted the label of the 1-arrow in the middle, which is the identity.

    Since

    is an identity for horizontal composition of 2-arrows, we deduce that ζ 1∘ζ 0\zeta_{1} \circ \zeta_{0} is obtained by pasting the 2-arrows in the following diagram. Both of the 1-arrows in the middle are the identity.

    Since

    is by definition an identity for vertical composition of 2-arrows, we deduce that ζ 1∘ζ 0\zeta_{1} \circ \zeta_{0} is obtained by pasting the 2-arrows in the following diagram.

    Appealing to the fact that

    is by definition an identity for vertical composition, and similarly that

    is by definition an identity for vertical composition, we deduce that ζ 1∘ζ 0\zeta_{1} \circ \zeta_{0} is obtained by pasting the 2-arrows in the following diagram. The leftmost of the two 1-arrows in the middle is f 1f_{1}, and the rightmost is f 0f_{0}.

    Carrying out the pasting of these 2-arrows first horizontally and then vertically, we deduce that ζ 1∘ζ 0\zeta_{1} \circ \zeta_{0} is obtained by pasting the 2-arrows in the following diagram, as we wished to show.

    • CommentRowNumber41.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    2) Let

    be a 2-arrow of 𝒞\mathcal{C}, let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 1-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    Let us demonstrate this. We make the following observations.

    I) We have that (g⋅ζ 1)∘(g⋅ζ 0)(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0}) is obtained by pasting the following 2-arrows. The 1-arrow in the middle is gg.

    By definition of g⋅ζ 1g \cdot \zeta_{1} and g⋅ζ 0g \cdot \zeta_{0}, we deduce that (g⋅ζ 1)∘(g⋅ζ 0)(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0}) is obtained by pasting the 2-arrows in the following diagram. The leftmost of the 1-arrows in the middle is the identity, and the rightmost is gg.

    By 1), we deduce that (g⋅ζ 1)∘(g⋅ζ 0)(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0}) is obtained by pasting the 2-arrows in the following diagram. The first from the left of the 1-arrows in the middle is f 1f_{1}, the second is f 0f_{0}, and the third is gg.

    II) Pasting together the 2-arrows

    we obtain g⋅ζ 0⋅f 1g \cdot \zeta_{0} \cdot f_{1}.

    III) Pasting together the 2-arrows

    gives the following 2-arrow.

    Pasting together the 2-arrows

    thus gives the 2-arrow obtained by pasting together the following 2-arrows, which is (g∘f 0)⋅f 1(g \circ f_{0}) \cdot f_{1}.

    It follows from I) - III) that (g⋅ζ 1)∘(g⋅ζ 0)(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0}) is obtained by pasting the following 2-arrows, as we wished to show. The 1-arrow in the middle is g∘f 0∘f 1g \circ f_{0} \circ f_{1}.

    • CommentRowNumber42.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    3) Let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 2-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    Let us demonstrate this. We make the following observations.

    I) We have that (ζ 1⋅f 1)∘ζ 0(\zeta_{1} \cdot f_{1}) \circ \zeta_{0} is obtained by pasting the following 2-arrows. The middle 1-arrow is f 1f_{1}.

    Since

    is an identity for horizontal composition, we deduce, appealing to the definition of ζ 1⋅f 1\zeta_{1} \cdot f_{1}, that (ζ 1⋅f 1)∘ζ 0(\zeta_{1} \cdot f_{1}) \circ \zeta_{0} is obtained by pasting the following 2-arrows. The leftmost 1-arrow in the middle is f 1f_{1}, and the rightmost is the identity.

    II) We obtain the same 2-arrow, namely ζ 0\zeta_{0}, by pasting of the 2-arrows

    as by pasting the following 2-arrows.

    III) We obtain the same 2-arrow, namely ζ 1\zeta_{1}, by pasting of the 2-arrows

    as by pasting the following 2-arrows.

    Carrying out the pasting of the 2-arrows

    by composing first vertically and then horizontally, we deduce that (ζ 1⋅f 1)∘ζ 0(\zeta_{1} \cdot f_{1}) \circ \zeta_{0} is obtained by pasting the following 2-arrows.

    Carrying out this pasting by composing first horizontally and then vertically, we conclude that (ζ 1⋅f 1)∘ζ 0(\zeta_{1} \cdot f_{1}) \circ \zeta_{0} is obtained by pasting the following 2-arrows, as we wished to show. The 1-arrow in the middle is f 2∘f 0f_{2} \circ f_{0}.

    • CommentRowNumber43.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    4) Let

    be a 2-arrow of 𝒞\mathcal{C}, let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 1-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    Let us demonstrate this. We make the following observations.

    I) We have that (f⋅ζ 1⋅g 0)∘((f∘f 1)⋅ζ 0)(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big) is obtained by pasting the following 2-arrows. The middle 1-arrow is f∘f 1∘g 0f \circ f_{1} \circ g_{0}.

    II) The 2-arrow

    can be obtained by pasting together the following 2-arrows.

    III) We deduce from I) and II), by the definition of the 2-arrows which make up the pasting diagram in I), that (f⋅ζ 1⋅g 0)∘((f∘f 1)⋅ζ 0)(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big) is obtained by pasting the following 2-arrows.

    IV) We obtain the same 2-arrow, namely ζ 0\zeta_{0}, by pasting of the 2-arrows

    as by pasting the following 2-arrows.

    V) We obtain the same 2-arrow, namely ζ 1\zeta_{1}, by pasting of the 2-arrows

    as by pasting the following 2-arrows.

    VI) By III) - V), we conclude that (f⋅ζ 1⋅g 0)∘((f∘f 1)⋅ζ 0)(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big) is obtained by pasting the following 2-arrows.

    VII) By pasting the 2-arrows

    we obtain the following 2-arrow.

    VIII) By pasting the 2-arrows

    we obtain the following 2-arrow.

    Pasting the 2-arrows

    we thus obtain the following 2-arrow.

    By VI) - VIII), we conclude that (f⋅ζ 1⋅g 0)∘((f∘f 1)⋅ζ 0)(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big) is obtained by pasting the following 2-arrows, as we wished to show.

    • CommentRowNumber44.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    5) Let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 2-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    This follows immediately from 4). Indeed, we let f 0f_{0}, f 1f_{1}, and ff in 4) all be

    We let g 0g_{0} in 4) be the 1-arrow f 1f_{1} that we have here, and let g 1g_{1} in 4) be the 1-arrow f 0f_{0} that we have here. We let ζ 0\zeta_{0} in 4) be the 2-arrow ζ 1\zeta_{1} that we have here, and let ζ 1\zeta_{1} in 4) be the 2-arrow ζ 0\zeta_{0} that we have here.

    6) Let

    be a 2-arrow of 𝒞\mathcal{C}, and let

    be a 2-arrow of 𝒞\mathcal{C}. Then the following diagram commutes.

    This follows immediately from 4). Indeed, we let f 0f_{0} in 4) be the 1-arrow f 0f_{0} that we have here, and let both f 1f_{1} and ff in 4) be

    We let g 0g_{0} and g 1g_{1} in 4) be the 1-arrows g 0g_{0} and g 1g_{1} that we have here respectively. We let ζ 0\zeta_{0} and ζ 1\zeta_{1} in 4) be the 2-arrows ζ 0\zeta_{0} and ζ 1\zeta_{1} that we have here respectively.

    • CommentRowNumber45.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 9th 2015
    • (edited Mar 16th 2015)

    We can now begin our demonstration that the diagram

    commutes.

    1) The following diagram commutes.

    The first square from the top commutes by 2) in #41. The second commutes by 3) in #42. The third commutes by 4) in #43. The fourth commutes by 4) in #43.

    2) The following diagram commutes.

    The first square from the top commutes by 5) in #44. The second commutes by 6) in #44. The third commutes by 4) in #43.

    3) By 1) and 2), we have that the following diagram commutes.

    The two unlabelled arrows (omitted for lack of space) are as follows.

    4) Since η\eta and ε\epsilon are the unit and counit natural transformations of the adjunction between Sd\mathsf{Sd} and Ex\mathsf{Ex}, the following diagram commutes.

    Hence the following diagram commutes.

    5) By 3) and 4), the following diagram commutes.

    6) The following diagram commutes.

    The first square from the top commutes by 3) in #42. The second commutes by 4) in #43. The third also commutes by 4) in #43.

    7) Since η 𝒜\eta_{\mathcal{A}} and ε 𝒜\epsilon_{\mathcal{A}} are the unit and counit natural transformations of the adjunction between SS and |−|\left| - \right|, the following diagram commutes.

    Hence the following diagram commutes.

    8) By 6) and 7), the following diagram commutes.

    9) We demonstrated earlier that the diagram

    commutes. Hence the following diagram commutes.

    10) We deduce from 8) and 9) that the following diagram commutes.

    11) We conclude from 5) and 10) that the following diagram commutes.

    In other words, the following diagram commutes, as we wished to show.

    In the next post, I’ll construct the natural transformations ρ n\rho_{n} for n≥2n \geq 2, and thereafter the natural transformation ρ\rho that we are aiming for.

    This concludes the post which began with #32.

1 to 45 of 45

  1.