The associativity of Join

We use the recursion principle for the triple join (from TriJoin.v) to prove the associativity of Join. We'll use the common technique of combining symmetry and a twist equivalence. Temporarily writing * for Join, symmetry says that A × B <~> B × A and the twist says that A × (B × C) <~> B × (A × C). From these we get a composite equivalence A × (B × C) <~> A × (C × B) <~> C × (A × B) <~> (A × B) × C. One advantage of this approach is that both symmetry and the twist are their own inverses, so there are fewer maps to define and fewer composites to prove are homotopic to the identity. Symmetry is proved in Join/Core.v.

The twist equivalence TriJoin A B C <~> TriJoin B A C

We prove the twist equivalence using the Yoneda lemma. The idea is that TriJoin A B C → P is equivalent (as a 0-groupoid) to TriJoinRecData A B C P, and the latter is very symmetrical by construction, which makes it easy to show that it is equivalent to TriJoinRecData B A C P. Going back along the first equivalence gets us to TriJoin B A C → P. These equivalences are natural in P, so the twist equivalence follows from the Yoneda lemma. First we define a map of 0-groupoids that will underlie the natural equivalence.

This map is its own inverse in the 1-category of 0-groupoids.

We get the twist natural equivalence on TriJoinRecData.

Combining with the recursion equivalence trijoin_rec_inv_natequiv and its inverse gives the twist natural equivalence between the representable functors.

The Yoneda lemma for 0-groupoid valued functors therefore gives us an equivalence between the representing objects. We mark this with a prime, since we'll use a homotopic map with a slightly simpler definition.

It has the nice property that the underlying function of the inverse is again equiv_trijoin_twist', with arguments permuted.

The definition we end up with is almost the same as the obvious one, but has some extra ap idmaps in it.

The next two give the obvious definition.

As an aside, note that trijoin_twist computes nicely on joinr.

The obvious definition is homotopic to the definition via the Yoneda lemma.

Both sides are trijoin_rec applied to TriJoinRecData:

Therefore the obvious definition is also an equivalence, and the inverse function can also be chosen to be trijoin_twist.

The associativity of Join

trijoin_twist corresponds to the permutation (1,2). The equivalence corresponding to the permutation (2,3) also plays a key role, so we name it here.

As a consequence, we get associativity of powers.

Naturality of trijoin_twist

Our goal is to prove that trijoin_twist A' B' C' o functor_join f (functor_join g h) is homotopic to functor_join g (functor_join f h) o trijoin_twist A B C. We first give a way to write anything of the form trijoin_rec f o trijoin_twist A B C as trijoin_rec applied to some TriJoinRecData.

Naturality of trijoin_twist. This version uses functor_trijoin and simply combines previous results.

And now a version using functor_join.

Naturality of trijoin_id_sym

Naturality of trijoin_id_sym, using functor_join. In this case, it's easier to do this version first.

Naturality of trijoin_id_sym, using functor_trijoin.

Naturality of join_assoc

Since join_assoc is a composite of join_sym, trijoin_twist and trijoin_id_sym, we just use their naturality.

The Triangle Law

The unitors were defined in Join/Core.v, since they do not require associativity. Here's a version of the triangle law expressed using trijoin_twist instead of join_assoc, and only using the right unitor. Since the left unitor is defined using join_sym, the usual triangle law follows.

The hexagon axiom

For the hexagon, we'll need to know how to compose trijoin_id_sym with something of the form trijoin_rec f. For some reason, the proof is harder than it was for trijoin_twist. This describes the transformation on TriJoinRecData corresponding to precomposition with trijoin_id_sym, as in the next result.

This is analogous to trijoin_rec_trijoin_twist above, with trijoin_twist replaced by trijoin_id_sym.

Here is our first hexagon law. This is not the usual hexagon axiom, but we will see that it is equivalent, and is itself useful. This law states that the following diagram commutes, where we write × for Join:

    A * (B * C) -> A * (C * B) -> C * (A * B)
        |                            |
        v                            v
    B * (A * C) -> B * (C * A) -> C * (B * A)

Here every arrow is either trijoin_twist _ _ _ or trijoin_id_sym _ _ _, and they alternate as you go around. These correspond to the permutations (1,2) and (2,3) in the symmetric group on three letters. We already know that they are their own inverses, i.e., they have order two. The above says that the composite (1,2)(2,3) has order three. These are the only relations in this presentation of S_3. Note also that every object in this diagram is parenthesized in the same way. That will be important in our proof.

Next we paste on a naturality square for join_sym on the right of the diagram:

    A * (B * C) -> A * (C * B) -> C * (A * B) -> (A * B) * C
        |                            |                |
        v                            v                v
    B * (A * C) -> B * (C * A) -> C * (B * A) -> (B * A) * C

The new horizontal maps are join_sym _ _ and the new vertical map is functor_join (join_sym A B) idmap. This makes both horizontal composites definitionally equal to join_assoc _ _ _, so the statement is about a square.

Finally, we paste on the defining square for join_assoc on the left to get the hexagon axiom for the symmetric monoidal structure:

    A * (C * B) -> A * (B * C) -> (A * B) * C
         |              |              |
         v              v              v
    (A * C) * B -> B * (A * C) -> (B * A) * C

The right-hand square is a horizontally-compressed version of the rectangle from the previous result, whose horizontal arrows are associativity. In the left-hand square, the new vertical map is join_assoc A C B and the horizontal maps are trijoin_id_sym A C B and join_sym (Join A C) B.