2. Background

Let us briefly introduce the key concepts of this paper: symmetric monoidal wild categories and smash products. We assume familiarity with HoTT and refer to the HoTT Book (The Univalent Foundations Program 2013) for the basic constructions and definitions used here. For the remainder of this paper, we adopt the convention that square-shaped diagrams denote (i) commutative squares of functions whenever their source is in the top-left corner and (ii) commutative squares of paths whenever their source is in the bottom-left corner. For instance, the left diagram below expresses the identity (of functions) $g \circ f = i \circ h$ , whereas the right diagram below expresses the identity (of paths) $p \cdot q = r \cdot s$ .

2.2 Smash products

The model of the smash product we use here is given by the cofibre of the inclusion $A \vee B \hookrightarrow A \times B$ , that is, the following (homotopy) pushout.

For the sake of clarity, let us spell this out in detail by giving explicit names to all constructors of $A \wedge B$ . We give the smash product the following self-contained definition.

Definition 5 (Smash products). The smash product of two pointed types $A$ and $B$ is the HIT generated by:

• • a point $\star _{\wedge } : A \wedge B$ ,

• • points ${{\langle a,b \rangle }} : A \wedge B$ for every pair $(a,b) : A \times B$ ,

• • paths ${{{\mathsf{push}}_{{\mathsf{l}}}}(a)}:{{\langle a,\star _B \rangle }} = \star _{\wedge }$ for every point $a : A$ ,

• • paths ${{{\mathsf{push}}_{{\mathsf{r}}}}(b)} :{{\langle \star _A,b \rangle }} = \star _{\wedge }$ for every point $b : B$ ,

• • a coherence ${{{\mathsf{push}}_{{\mathsf{lr}}}}} :{{{\mathsf{push}}_{{\mathsf{l}}}}(\star _A)} ={{{\mathsf{push}}_{{\mathsf{r}}}}(\star _B)}$ .

We always take $A \wedge B$ to be pointed by $\star _{\wedge }$ .

Remark 6. We remark that we could equivalently have defined the smash product by the following pushout.

This definition has the advantage of not having any $2$ -dimensional path constructors but has the disadvantage of having an additional point constructor. It turns out that Definition 5 suits our purposes better, so we stick with it. Alternatively, we could have defined the smash product to have ${\langle \star _A,\star _B \rangle }$ as its canonical basepoint. Such a definition is obtained by forming the HIT generated by:

• • points ${{\langle a,b \rangle }} : A \wedge B$ for every pair $(a,b) : A \times B$ ,

• • paths ${{{\mathsf{push}}_{{\mathsf{l}}}}(a)}:{{\langle a,\star _B \rangle }} ={{\langle \star _A,\star _B \rangle }}$ for every point $a : A$ ,

• • paths ${{{\mathsf{push}}_{{\mathsf{r}}}}(b)} :{{\langle \star _A,b \rangle }} ={{\langle \star _A,\star _B \rangle }}$ for every point $b : B$ ,

• • a coherence ${{{\mathsf{push}}_{{\mathsf{lr}}}}} :{{{\mathsf{push}}_{{\mathsf{l}}}}(\star _A)} ={{{\mathsf{push}}_{{\mathsf{r}}}}(\star _B)}$ ,

• • a coherence $\mathsf{push}_{\mathsf{l}\star } :{{{\mathsf{push}}_{{\mathsf{l}}}}(\star _A)} = \mathsf{refl}$ .

It was suggested to us by an anonymous reviewer that this definition could allow certain statements in this paper to be expressed in a slightly less convoluted way (in particular Lemmas 19 and 20 ). We stick to Definition 5 as it is more commonly used in the HoTT literature but remark that the interested reader may find it enlightening to reinterpret the results of this paper in terms of the definition above.

Let us verify that the smash product is functorial. In what follows, a pointed function $A \to _\star B$ is a function $f : A \to B$ equipped with a proof of pointedness $\star _f : f(\star _A) = \star _B$ .

Definition 7. For two pointed functions $f : A \to _\star C$ and $g : B \to _\star D$ , there is an induced map $f \wedge g : A \wedge B \to _\star C \wedge D$ defined on point constructors by:

\begin{align*} (f \wedge g)\,(\star _{\wedge }) &= \star _{\wedge }\\ (f \wedge g)\,\langle a,b\rangle &= \langle f(a),g(b)\rangle \end{align*}

and on ( $1$ -dimensional) path constructors by the following compositions:

\begin{align*}{\mathsf{ap}}_{f \wedge g}{({{{\mathsf{push}}_{{\mathsf{l}}}}(a)})} \,\,\, &=\,\,\, \langle f(a),g(\star _B)\rangle \xrightarrow{{\mathsf{ap}}_{\langle f(a), - \rangle }{(\star _g)}} \langle f(a),\star _D\rangle \xrightarrow{{{{\mathsf{push}}_{{\mathsf{l}}}}(f(a))}} \star _{\wedge } \\{\mathsf{ap}}_{f \wedge g}{({{{\mathsf{push}}_{{\mathsf{r}}}}(b)})} \,\,\, &=\,\,\, \langle f(\star _A),g(b)\rangle \xrightarrow{{\mathsf{ap}}_{\langle -,g(b) \rangle }{(\star _f)}} \langle \star _C, g(b)\rangle \xrightarrow{{{{\mathsf{push}}_{{\mathsf{r}}}}(g(b))}} \star _{\wedge } \end{align*}

The final case of the definition, that is, ${\mathsf{ap}}_{\mathsf{ap}_{f \wedge g}}{({{{\mathsf{push}}_{{\mathsf{lr}}}}})}$ , is a simple coherence which does not matter in the remainder of the paper. We take $f \wedge g$ to be pointed by $\mathsf{refl}$ .

We also take the opportunity to mention the commutativity of smash products. This is trivial since the definition of $A \wedge B$ is entirely symmetric in both arguments.

Proposition 8. The swap map $A \times B \to B \times A$ induces a pointed equivalence $A \wedge B \simeq _\star B \wedge A$ .

3. Associativity

Proving that the smash product is associative is far less straightforward than proving that it is commutative. In fact, even the seemingly direct task of constructing the associator map is no mean feat. While associativity has already been verified by van Doorn (Reference van Doorn2018) and, using a computer-generated proof, by Brunerie (Reference Brunerie2018), let us give a direct construction of the equivalence. We do this because an explicit description makes the associator easier to trace when verifying, for example, the pentagon identity. For this purpose, let us introduce a new HIT capturing double smash products in a way which is neutral with respect to the distribution of parentheses.

Table 1. $(A \wedge B) \wedge C$ vs. $\bigwedge (A,B,C)$

Let us verify that this actually captures a double smash product. What we need is an equivalence $(A \wedge B) \wedge C \simeq \bigwedge (A,B,C)$ . The underlying map of this equivalence is described in Table 1 with constructors of $(A \wedge B) \wedge C$ on the left and the corresponding constructors of $\bigwedge (A,B,C)$ on the right. We remark that this correspondence only serves as an informal sketch of the function – in practice, some simple coherences are needed for the higher constructors to make it well typed. Verifying that this map indeed defines an equivalence is somewhat laborious but direct; the interested reader is referred to the computer formalisation. We get the associativity of the smash product as a consequence.

Proof. Observe that $\bigwedge (A,B,C)$ is trivially invariant under permutation of the arguments in the sense that, for example, $\bigwedge (A,B,C) \simeq \bigwedge (B,C,A)$ . This allows us to define $\alpha _{A,B,C}$ by the following composition of equivalences:

\begin{align*} (A \wedge B) \wedge C \simeq \bigwedge (A,B,C) \simeq \bigwedge (B,C,A) \simeq (B \wedge C) \wedge A \simeq A \wedge (B \wedge C) \end{align*}

The fact that $\alpha _{A,B,C}$ is pointed holds by $\mathsf{refl}$ .

4. The Heuristic

Reasoning about functions defined over iterated smash products quickly gets out of hand. For instance, in order to verify the pentagon axiom, we need to reason about functions on the form $((A \wedge B) \wedge C) \wedge D \to E$ . To prove an equality of two such functions $f$ and $g$ , we have to construct, for instance, a dependent path:

(2)

which boils down to filling a $4$ -dimensional cube with highly non-trivial sides. This is often completely unmanageable in practice. The best thing we can hope for is that these types of coherence problems are, in some sense, automatic. This was, in fact, suggested by Brunerie (Reference Brunerie2016) but was never proved nor in any way made formal. In this section, we will see that this, in fact, is the case.

The first troublesome part of verifying equalities of functions defined over smash products is the ${{\mathsf{push}}_{{\mathsf{lr}}}}$ constructor. Fortunately, we do not have to deal with it. Let us denote by ${A}\,\widetilde{\wedge }\,{B}$ the exact same HIT as $A \wedge B$ but with the ${{\mathsf{push}}_{{\mathsf{lr}}}}$ constructor removed. In other words, it is the following pushout.

Let $i$ be the obvious map ${A}\,\widetilde{\wedge }\,{B}\to A \wedge B$ .

Proof. The antecedent of the statement provides us with

• • a path $p : f(\star _{\wedge }) = g (\star _{\wedge })$ ,

• • a homotopy $h : ((a,b) : A \times B) \to f \langle a,b\rangle = g \langle a,b \rangle$ ,

• • for each $a : A$ , a filler $h_l(a)$ of the square

  

• • for each $b : B$ , a filler $h_r(b)$ of the square

  

To prove that $f = g$ , we need to provide $p^{\prime},h^{\prime},h_l^{\prime},h_r^{\prime}$ of the same types as above, as well as a filler $h^{\prime}_{lr}$ of the cube

where the top and bottom squares are given, respectively, by $\mathsf{ap}_{\mathsf{ap}_{g}}({{{\mathsf{push}}_{{\mathsf{lr}}}}})$ and $\mathsf{ap}_{\mathsf{ap}_{f}}({{{\mathsf{push}}_{{\mathsf{lr}}}}})$ , the left- and right-hand side, respectively, by $\mathsf{refl}_{h^{\prime}(\star _A,\star _B)}$ and $\mathsf{refl}_{p^{\prime}}$ and the front and back, respectively, by $h_l^{\prime}(\star _A)$ and $h_r^{\prime}(\star _B)$ .

We set $p^{\prime} := p$ , $h^{\prime} := h$ and $h_l^{\prime} := h_l$ . For $h_r^{\prime}$ , however, we need to make an alteration. We construct it as the following composite square

where the square on the left is $h_r(b)$ and the square on the right is the lid of the cube

with $h_l(\star _A)$ and $h_r(\star _B)$ as left- and right-hand sides, the action of $f$ and $g$ on ${{\mathsf{push}}_{{\mathsf{lr}}}}$ on the front and back, and $\mathsf{refl}_{h(\star _A,\star _B)}$ on the bottom. One can now easily construct the filler $h^{\prime}_{lr}$ by generalising the cubes involved and applying path induction.

Remark 12. Lemma 11 is a special case of the more general statement that $i$ is a retraction (this was called to our attention by Dan Petersen). In fact, there is an equivalence ${A}\,\widetilde{\wedge }\,{B} \simeq S^1 \vee (A \wedge B)$ under which the map $i$ becomes the canonical retraction $S^1 \vee (A \wedge B) \to A \wedge B$ . To see this, consider the following commutative diagram.

By taking pushouts of the rows, we produce the span $1 \leftarrow A + B \to A \times B$ , the pushout of which is ${A}\,\widetilde{\wedge }\,{B}$ . On the other hand, by taking pushouts of the columns, we produce the span $S^1 \leftarrow 1 \rightarrow A \wedge B$ , the pushout of which is $S^1 \vee (A \wedge B)$ . This yields the desired equivalence ${A}\,\widetilde{\wedge }\,{B} \simeq S^1 \vee (A \wedge B)$ by the 3 $\times$ 3-lemma (introduced by Brunerie Reference Brunerie2016, Lemma 1.8.3 with computer formalisation by Pujet and Mörtberg Reference Pujet and Mörtberg2020). The fact that $i$ factors in the appropriate manner follows by construction. Thus, we have given an alternative proof of Lemma 11.

Lemma11 is useful but does not get us all the way. Complicated paths like (2) still need to be constructed, regardless of what happens with the ${{\mathsf{push}}_{{\mathsf{lr}}}}$ constructor. To strengthen the principle, we will need to introduce the concept of homogeneous types which, to the best of our knowledge, was first introduced (in HoTT) by Kraus (Reference Kraus2013).

The usefulness of homogeneous types is showcased by the following lemma which was first conjectured for Eilenberg–MacLane spaces in work leading up to Brunerie et al. (Reference Brunerie, Ljungström, Mörtberg, Manea and Simpson2022) and later proved and generalised by Cavallo (Reference Cavallo2021b) (and later further generalised by Buchholtz et al. Reference Buchholtz, Christensen, Flaten and Rijke2023).

The same lemma holds for bi-pointed functions $f,g : A \to _\star (B \to _\star C)$ , since the type $(B \to _\star C)$ is homogeneous if $C$ is. This gives a corresponding principle for maps defined over smash products via the adjunction $(A \wedge B \to _\star C) \simeq (A \to _\star (B \to _\star C))$ .

The following form is useful when dealing with non-pointed functions.

Proof. Let $h(a,b) : f\langle a,b \rangle = g \langle a, b \rangle$ . We know that $g(\star _{\wedge }) = f(\star _{\wedge })$ by the composite path

\begin{equation*}g(\star _{\wedge }) \xrightarrow {{\mathsf {ap}}_{g}{({{{\mathsf {push}}_{{\mathsf {l}}}}(\star _A)})}^{-1}} g\langle \star _A,\star _B \rangle \xrightarrow {h(\star _A,\star _B)^{-1}}{f\langle \star _A,\star _B \rangle } \xrightarrow {{\mathsf {ap}}_{f}{({{{\mathsf {push}}_{{\mathsf {l}}}}(\star _A)})}} f (\star _{\wedge }) \end{equation*}

Hence, we may view both $f$ and $g$ as pointed functions $A \wedge B \to _\star (C,f(\star _{\wedge }))$ . Now, Lemma15 applies and, in particular, $f = g$ as plain functions.

If we could apply Lemma15 or 16 when proving the pentagon identity, we would be done immediately. Unfortunately, none of the types showing up in the statement of the pentagon identity are necessarily homogeneous. There is, however, some use for the lemmas. Let us first make the following observation: given two pointed functions $f,g: A \wedge B \to _\star C$ and a homotopy $h : ((a, b) : A \times B) \to f\langle a,b\rangle = g \langle a,b \rangle$ , we can define two functions $L_h : A \to \Omega (C)$ and $R_h : B \to \Omega (C)$ in terms of $h$ and ${{\mathsf{push}}_{{\mathsf{l}}}}$ / ${{\mathsf{push}}_{{\mathsf{r}}}}$ . The obvious definition of these maps (which we will spell out in Definition17) will give us a version of Lemma11 which tells us that if $L_h$ and $R_h$ are constant, then $f = g$ as plain functions. Now, if either $A$ or $B$ is another smash product, this would be a situation where Lemma16 applies since $\Omega (C)$ (and indeed any path type) is homogeneous. This suggests that Lemma16 may be used our advantage when dealing with iterated smash products. Let us try to spell this out more clearly. We can state the idea without any pointedness assumptions by simply replacing $\Omega (C)$ with the path type $f(\star _{\wedge }) = g(\star _{\wedge })$ which is also homogeneous (and agrees with $\Omega (C)$ whenever $f$ and $g$ are pointed).

Definition 17. Let $f,g : A \wedge B \to C$ and let $h : ((a, b) : A \times B) \to f{{\langle a,b \rangle }} = g{{\langle a,b \rangle }}$ . This induces functions $L_h : A \to f(\star _{\wedge }) = g(\star _{\wedge })$ and $R_h : B \to f(\star _{\wedge }) = g(\star _{\wedge })$ defined by:

\begin{align*} L_h(a) &={\mathsf{ap}}_{f}{({{{\mathsf{push}}_{{\mathsf{l}}}}(a)})}^{-1} \cdot h(a,\star _B) \cdot{\mathsf{ap}}_{g}{({{{\mathsf{push}}_{{\mathsf{l}}}}(a)})} \\ R_h(b) &={\mathsf{ap}}_{f}{({{{\mathsf{push}}_{{\mathsf{r}}}}(b)})}^{-1} \cdot h(\star _A,b) \cdot{\mathsf{ap}}_{g}{({{{\mathsf{push}}_{{\mathsf{r}}}}(b)})} \end{align*}

We may use $L_h$ and $R_h$ to give a compact induction principle for identities $f = g$ . The following lemma is a direct rewriting of Lemma11.

The key idea now is, we stress again, to use Lemmas18 and 15/16 iteratively to prove equalities of functions defined over iterated smash products. As a first example, let us consider the problem of proving an equality of functions $f = g$ where $f, g : (A \wedge B) \wedge C \to D$ . The following lemma provides a good estimate of the minimal amount of data needed to construct such an equality.

For completeness, let us state the corresponding lemma for functions $f, g : ((A \wedge B) \wedge C) \wedge D \to E$ , as these appear in the pentagon identity. The proof is by Lemmas18,16 and 19, following the exact same line of attack as before. We acknowledge that the following result is highly technical but stress that the interesting aspect of it is not the exact details of the statement; rather, we include it to showcase the fact that only squares are involved, as opposed to the (many) high-dimensional cubes of coherences which would appear in a naive inductive proof.

Let us make three observations about Lemmas19 and 20:

1. 1. In both statements, the different pieces of data are almost completely mutually independent. The only meaningful choice we can make is that of the homotopy $h$ . This means that we are free to provide any proofs we like for the remaining steps without having to worry about future coherences.

2. 2. In many concrete cases (especially those relating to the symmetric monoidal structure of the smash product), the homotopy $h$ will be defined by $h(a_1,\dots, a_n) := \mathsf{refl}$ . This means that all other data we need to provide are equalities of composite paths defined entirely in terms of applications of $f$ and $g$ on ${{\mathsf{push}}_{{\mathsf{l}}}}$ and ${{\mathsf{push}}_{{\mathsf{r}}}}$ – something we can usually simply unfold to something (hopefully) simple.

3. 3. Going from Lemmas19–20, we see that only two additional assumptions are needed. If we were to increase the number of copies of smash products appearing in the domain by one, we would only need to provide two additional squares (and still no higher coherences). Hence, the complexity of such proofs grows linearly with the complexity of the domain. For comparison, if we were to resort to a naive proof by a deep smash product induction, the amount of data needed would grow exponentially.

While it is possible to generalise Lemmas19 and 20 to a statement concerning $n$ -fold smash products, let us, for now, only summarise the fundamental idea behind Lemmas19 and 20 in terms of an informal heuristic.

Heuristic 21. To show that two functions $f,g : \bigwedge _{i \leq n} A_i \to B$ are equal, it suffices, by iterative application Lemmas 18, 16 and 14, to provide a family of paths $h(x_1,\dots, x_n) : f \langle x_1,\dots, x_n \rangle = g \langle x_1, \dots, x_n\rangle$ for $x_i : A_i$ and to show that it is coherent with $f$ and $g$ on any single application of ${{\mathsf{push}}_{{\mathsf{l}}}}$ or ${{\mathsf{push}}_{{\mathsf{r}}}}$ (e.g., ${\mathsf{ap}}_{\langle -,x_{i+1},\dots, x_n\rangle }{({{{\mathsf{push}}_{{\mathsf{l}}}}} \langle x_1,\dots, x_{i-1} \rangle )}$ . Furthermore, if an equality of pointed functions is required, we need to provide a filler of the following square:

The reader who is looking for a precise mathematical statement of the above is referred to Section 6 where we also introduce some additional machinery required to make the idea formal. For now, we will settle for this informal heuristic – in practice, when working with functions over a small fixed number of smash products, we do not quite need the full strength of a general theorem.

5. The Symmetric Monoidal Structure

Let us reap the fruits of our labour and show that the smash product defines a (1-coherent) symmetric monoidal product on the universe of pointed types. We will not verify all axioms here, since this is neither very instructive nor very interesting. Instead, we sketch the proofs of the two most technical properties and refer the interested reader to the computer formalisation.

Proposition 22. The smash product satisfies the hexagon identity, that is, we have an equality of pointed functions $H_0 = H_1$ where $H_0$ and $H_1$ are defined as the composites of each side of the following hexagon.

Proposition 23. The pentagon identity holds for the smash product, that is, we have an equality of pointed functions $P_0 = P_1$ where $P_0$ and $P_1$ are defined as the composites of each side of the following pentagon.

All other axioms defining a symmetric monoidal wild category follow in the same direct manner and we, after some rather mechanical labour (see computer formalisation), easily arrive at the main result.

5.1 Back to Brunerie’s thesis

A first consequence of the fact that Theorem24 finally has a complete and computer formalised proof is the correctness of Brunerie’s PhD thesis (2016). While a computer formalisation of the main results of the thesis was presented by Ljungström and Mörtberg (Reference Ljungström and Mörtberg2023), this formalisation did not stay completely true to Brunerie’s original proof. Indeed, certain proofs and constructions were reworked in order not to rely on results concerning smash products. Most notably, the cup product was redefined using an alternative definition by Brunerie et al. (Reference Brunerie, Ljungström, Mörtberg, Manea and Simpson2022, Section 4.1). In Brunerie’s thesis, the cup product (on integral Eilenberg–MacLane spaces) is defined as a map $\smile : K(\mathbb{Z},n)\wedge K(\mathbb{Z},m) \to{K(\mathbb{Z},n+m)}$ where, for $n, m \geq 1$ , we have $K(\mathbb{Z},n) := \lVert S^n\rVert _{n}$ , that is, the $n$ -truncation of the $n$ -sphere. Here, we define $S^n := \Sigma ^{n+1}(\emptyset )$ , that is, it is the $(n+1)$ -fold suspension of the empty type, where, recall, the suspension of a type $A$ , is the HIT $\Sigma (A)$ generated by

• • two points $\mathsf{north},\mathsf{south} : \Sigma (A)$ ,

• • paths $\mathsf{merid}\;{(a)} : \mathsf{north} = \mathsf{south}$ for each $a:A$ .

Brunerie’s construction of the cup product is by means of a lift from the corresponding map on spheres.

Above, the map $\wedge _{n,m} : S^n \wedge S^m \to S^{n+m}$ is the canonical equivalence defined in, for example, Brunerie (Reference Brunerie2016, Proposition 4.2.2). With this construction, most properties of the cup product can be shown by showing that the corresponding properties hold for $\wedge _{n,m}$ . In particular, graded-commutativity and associativity follow, respectively, from the following two propositions.

Proposition 25 (Brunerie Reference Brunerie2016, Proposition 4.2.4). The following diagram commutes.

where $(-1) : S^n \to S^n$ is defined by sending $\mathsf{merid}\;{(a)}$ to $\mathsf{merid}\;{(a)}^{-1}$ .

Proposition 26 (Brunerie Reference Brunerie2016, Proposition 4.2.2). The following diagram commutes.

These results are proved by Brunerie using proofs which rely on the symmetric monoidal structure of the smash product. While Proposition25 should be provable using the partial proof of symmetric monoidality due to van Doorn (Reference van Doorn2018, Section 4.3), Brunerie’s proof of Proposition26 relies on the pentagon identity which, until now, has been open. Thus, with Theorem24 we can finally conclude the following.

Theorem 27. The cup product, as constructed in Brunerie (Reference Brunerie2016, Definition 5.1.6), forms a graded-commutative and associative multiplication $K(\mathbb{Z},n) \wedge K(\mathbb{Z},m) \to K(\mathbb{Z},n+m)$ .

We remark that we have not provided a computer formalisation of the above since there already exist well-developed computer formalisations of the cup product and cohomology rings (Brunerie et al. Reference Brunerie, Ljungström, Mörtberg, Manea and Simpson2022; Lamiaux et al. Reference Lamiaux, Ljungström and Mörtberg2023; Ljungström and Mörtberg Reference Ljungström and Mörtberg2024).

6. A Formal Statement of the Heuristic

In a classical setting, the iterated smash product $\bigwedge _{i \leq n}{A_i}$ can be described as the quotient space $(A_0 \times \dots \times A_{n}) /{{\mathsf{FW}_{i\leq n}(A_i)}}$ where

\begin{equation*}{{\mathsf {FW}_{i\leq n}(A_i)}} := \{(a_0,\dots, a_{n}) \mid a_i = \star _{A_i} \text { for some $i$} \}\subset A_0 \times \dots \times A_{n}\end{equation*}

It is unclear how to mimic this construction in HoTT in a useful way, as the naive definition forces us to add, in a systematic way, an exponential number of higher coherences. However, the naive definition may still prove useful. Here, by ‘naive definition’, we mean the disjoint union

\begin{align*}{{{\mathsf{FS}}_{i \leq n}(A_i)}} := \bigsqcup _{i \leq n}\left (A^{(i)}_{0} \times \dots \times A^{(i)}_{n} \right )\qquad &\mathsf{ where }\hspace{.2cm}A^{(i)}_j = \begin{cases} A_j & \text{ if $i \neq j$}\\ 1 & \text{ if $i = j$} \end{cases} \end{align*}

While the cofibre of the canonical map ${{{\mathsf{FS}}_{i \leq n}(A_i)}} \to A_0 \times \dots \times A_{n}$ does not quite give us $\bigwedge _{i \leq n}{A_i}$ , it does, however, provide a useful approximation. This is, in fact, precisely the content of our heuristic. We will soon make this precise. Before this, let us give a less set-theoretic definition of ${{\mathsf{FS}}_{i \leq n}(A_i)}$ which is easier to work with in HoTT.

Definition 28. Given pointed types $A_0,\dots, A_{n}$ , we define ${{\mathsf{FS}}_{i\leq n}(A_i)}$ by induction on $n$ as follows.

\begin{equation*} {{{\mathsf {FS}}_{i\leq n}(A_i)}} := \begin {cases} 1 & \text { if $n = 0$}\\ ({{{\mathsf {FS}}_{i\leq {n-1}}(A_i)}} \times A_{n}) + (A_0\times \dots \times {A_{n-1}}) & \text { if $n \gt 0$} \end {cases} \end{equation*}

Let us, for clarity, explicitly describe the canonical map $\gamma _n :{{{\mathsf{FS}}_{i\leq n}(A_i)}} \to A_0 \times \dots \times A_n$ . It is recursively defined with $\gamma _0 : 1 \to A_0$ picking out the basepoint $\star _{A_{0}}$ and

\begin{equation*} \gamma _{n} : ({{{\mathsf {FS}}_{i\leq {n-1}}(A_i)}} \times A_{n}) + (A_0\times \dots \times {A_{n-1}}) \to A_0\times \dots \times A_n \end{equation*}

being defined by $\gamma _n = \gamma _n^{(1)} + \gamma _{n}^{(2)}$ where

\begin{align*} \gamma _n^{(1)}(x,a_{n}) &= (\gamma _{n-1}(x),a_n)\\ \gamma _n^{(2)}(a_0,\dots, a_{n-1}) &= (a_0,\dots, a_{n-1},\star{A_{n}}) \end{align*}

Definition 29. Given pointed types $A_0,\dots, A_n$ , we define $\widetilde{\bigwedge }_{i \leq n}{A_i}$ to be the cofibre of $\gamma _n :{{{\mathsf{FS}}_{i\leq n}(A_i)}} \to A_0 \times \dots \times A_n$ , that is, the following pushout.

We give its constructors explicit names and write

• • $\star _{\widetilde{\wedge }}$ for its basepoint,

• • $\langle a_0,\dots, a_n \rangle$ for its underlying points,

• • ${{{\mathsf{push}}}}^{(1)}(x) : \langle \gamma _n^{(1)}(x) \rangle = \star _{\widetilde{\wedge }}$ for the first coherence given by the pushout square,

• • ${{{\mathsf{push}}}}^{(2)}(x) : \langle \gamma _n^{(2)}(x) \rangle = \star _{\widetilde{\wedge }}$ for the second coherence given by the pushout square.

It is easy to see that the composition ${{{\mathsf{FS}}_{i \leq n}(A_i)}} \to A_0\times \dots \times A_n \to \bigwedge _{i \leq n}{A_i}$ is null-homotopic. Hence, there is a basepoint preserving inclusion (of constructors) $\iota : \widetilde{\bigwedge }_{i \leq n}{A_i} \to \bigwedge _{i \leq n}{A_i}$ s.t. $\iota \langle a_0,\dots, a_n\rangle = \langle a_0,\dots, a_n\rangle$ .

We also remark that there is an inclusion $\uparrow : \left (\widetilde{\bigwedge }_{i \leq{n-1}}{A_i}\right )\times A_{n} \to \widetilde{\bigwedge }_{i \leq{n}}{A_i}$ . It is defined by:

\begin{align*} \uparrow (\star _{\widetilde{\wedge }},a_n) &:= \star _{\widetilde{\wedge }}\\ \uparrow (\langle a_0,\dots, a_{n-1} \rangle, a_n) &:= \langle a_0,\dots, a_n \rangle \\{\mathsf{ap}}_{\uparrow (-,a_n)}{({{{{\mathsf{push}}}(x)}})} &:={{{\mathsf{push}}}}^{(1)}{(x,a_n)} \end{align*}

Furthermore, $\uparrow$ commutes with $\iota$ in the sense that, for $x : \widetilde{\bigwedge }_{i \leq{n-1}}{A_i}$ and $a_n : A_{n}$ , we have the following path (in $\bigwedge _{i \leq n}{A_i}$ ):

\begin{equation*}\uparrow ^{\mathsf {coh}}(x, a_n) \,: \iota \left (\uparrow (x,a_n)\right ) = \langle \iota (x), a_n \rangle \end{equation*}

One constructs $\uparrow ^{\mathsf{coh}}(x, a_n)$ very directly by induction on $x$ . Let us give the construction when $x$ is a point constructor. When $x:=\langle a_0,\dots, a_{n-1} \rangle$ , the statement holds by $\mathsf{refl}$ . When $x:=\star _{\widetilde{\wedge }}$ , the type of $\uparrow ^{\mathsf{coh}}(x, a_n)$ reduces to $\star _{\wedge } = \langle \star _{\wedge },a_n \rangle$ which holds by ${{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)}^{-1}$ . Hence, we define

(3) \begin{align} \uparrow ^{\mathsf{coh}}(\langle a_0,\dots, a_{n-1} \rangle, a_n) & :=\mathsf{refl} \\[-3pt] \nonumber \end{align}

(4) \begin{align} \uparrow ^{\mathsf{coh}}(\star _{\widetilde{\wedge }}, a_n)& :={{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)}^{-1} \\[15pt] \nonumber \end{align}

The higher coherence is very straightforward and we omit it for the sake of readability. We are now ready for the key result of the section. It makes precise to what extent $\widetilde{\bigwedge }_{i \leq n}{A_i}$ approximates ${\bigwedge }_{i \leq n}{A_i}$ and may be seen as a formal version of our heuristic. We will later restate the result in a less technical and more self-contained form.

Theorem 30. Let $f, g : \wedge _{i \leq n} A_i \to B$ . Given a homotopy $\widetilde{p}_n : (x : \widetilde{\bigwedge }_{i \leq n} A_i) \to f(\iota (x)) = g(\iota (x))$ , there is a homotopy $p_n : (x : \wedge _{i \leq n} A_i) \to f(x) = g(x)$ . Furthermore, $p_n$ satisfies:

(5) \begin{align} p_n(\star _{\wedge }) &= \widetilde{p}_n(\star _{\widetilde{\wedge }}) \\[-3pt] \nonumber \end{align}

(6) \begin{align} p_n \langle a_0,\dots, a_n\rangle &= \widetilde{p}_n \langle a_0,\dots, a_n\rangle \\[15pt] \nonumber \end{align}

Proof. We proceed by induction on $n$ . When $n=0$ , the map $\iota$ is simply the canonical equivalence between the cofibre of the unique pointed map $1 \to _\star A_0$ and $A_0$ itself, and the theorem is trivial.

Let $n \geq 1$ and let $f$ , $g$ and $\widetilde{p}_n$ be as in the theorem statement. Let us, for clarity, rewrite the domain of $f$ and $g$ as the binary smash product $\left (\bigwedge _{i \leq{n-1}} A_{i}\right ) \wedge A_n$ . In order to construct $p_n : (x : \left (\bigwedge _{i \leq{n-1}} A_{i}\right ) \wedge A_n) \to f(x) = g(x)$ , it suffices, by Lemma11, to define

1. (a) a path $p_n(\star _{\wedge }) : f(\star _{\wedge }) = g(\star _{\wedge })$ ,

2. (b) for $a_n : A_n$ , homotopies $p_n\langle -, a_n \rangle : (x : \bigwedge _{i \leq{n-1}} A_{i}) \to f\langle x, y \rangle = g\langle x, y \rangle$ ,

3. (c) For each $a_n: A_n$ , a filler of the square

   

4. (d) For each $x: \bigwedge _{i \leq n-1}{A_i}$ , a filler of the square

   

For (a), we know that $\iota (\star _{\widetilde{\wedge }}) := \star _{\wedge }$ and thus $\widetilde{p}_n(\star _{\widetilde{\wedge }}) : f(\star _{\wedge }) = g(\star _{\wedge })$ . Consequently, we may simply set $p_n(\star _{\wedge }) := \widetilde{p}_n(\star _{\widetilde{\wedge }})$ . Doing so, (5) holds definitionally. For (b), we fix $a_n : A_n$ . By the induction hypothesis, it suffices to construct $p_n\langle \iota (x),a_n\rangle : f\langle \iota (x), y \rangle = g\langle \iota (x), y \rangle$ for $x : \widetilde{\bigwedge }_{i \leq n-1}{A_i}$ . We do this by the composite path

This completes the construction of $p_n \langle -, a_n\rangle$ . Note that, since $p_n \langle -, a_n\rangle$ was constructed using the induction hypothesis, we also get the following from (5):

\begin{align*} p_n \langle \star _{\wedge }, a_n \rangle &={\mathsf{ap}}_{f}{(\uparrow ^{\mathsf{coh}}(\star _{\wedge },a_n))}^{-1} \cdot{\widetilde{p}_n(\uparrow (\star _{\wedge },a_n))} \cdot{\mathsf{ap}}_{g}{(\uparrow ^{\mathsf{coh}}(\star _{\wedge },a_n))} & \text{ by (5)}\\ &={\mathsf{ap}}_{f}{({{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)})} \cdot p_n(\star _{\wedge }) \cdot{\mathsf{ap}}_{g}{({{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)})}^{-1} &\text{ by (4)} \end{align*}

and the following from (6):

\begin{align*} p_n \langle \vec{a}_{n-1}, a_n \rangle &={\mathsf{ap}}_{f}{(\uparrow ^{\mathsf{coh}}(\vec{a}_{n-1}, a_n))}^{-1} \cdot{\widetilde{p}_n(\uparrow (\vec{a}_{n-1}, a_n))} \cdot{\mathsf{ap}}_{g}{(\uparrow ^{\mathsf{coh}}(\vec{a}_{n-1},a_n))} & \text{ by (6)}\\ &= \mathsf{refl} \cdot \widetilde{p}_n(\vec{a}_{n-1},a_n) \cdot \mathsf{refl} &\text{ by (3)}\\ &= \widetilde{p}_n(\vec{a}_{n-1},a_n) \end{align*}

where $\vec{a}_{n-1}$ is short for $\langle a_0,\dots, a_{n-1} \rangle$ . So, to summarise, we have the following two identities for $p\langle -, a_n \rangle$ :

(7) \begin{align} p_n \langle \star _{\wedge }, a_n \rangle ={\mathsf{ap}}_{f}{({{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)})} \cdot p_n(\star _{\wedge }) \cdot{\mathsf{ap}}_{g}{({{{\mathsf{push}}_{{\mathsf{r}}}}(a_n)})}^{-1} \\[-3pt] \nonumber \end{align}

(8) \begin{align} p_n \langle \langle a_0,\dots, a_{n-1}\rangle, a_n \rangle = \widetilde{p}_n \langle a_0,\dots, a_{n-1}, a_n \rangle \\[15pt] \nonumber \end{align}

Note that, in particular, the latter identity verifies (6). Let us now turn to (c). By (7), we simply need to fill the square

which is entirely trivial by definition of path composition.

Finally, let us provide the data asked for in (d). Filling the square is equivalent to constructing, a homotopy $(x : \bigwedge _{i\leq n -1} A_i) \to \mathsf{left}(x) = \mathsf{right}(x)$ where $\mathsf{left},\mathsf{right} : \bigwedge _{i\leq n -1} A_i \to f(\star _{\wedge }) = g(\star _{\wedge })$ are defined by:

\begin{align*} \mathsf{left}(x) &:= p_n(\star _{\wedge })\\ \mathsf{right}(x) &:={\mathsf{ap}}_{f}{({{{\mathsf{push}}_{{\mathsf{l}}}}(x)})}^{-1} \cdot p_n\langle x,\star _{A_n} \rangle \cdot{\mathsf{ap}}_{g}{({{{\mathsf{push}}_{{\mathsf{l}}}}(x)})} \end{align*}

The codomain $f(\star _{\wedge }) = g(\star _{\wedge })$ is homogeneous (with $\mathsf{left}(\star _{\wedge })$ as basepoint) and thus Lemma16 applies. Hence, we only need to show that

\begin{equation*}\mathsf {left}\langle a_0, \dots, a_{n-1} \rangle = \mathsf {right}\langle a_0, \dots, a_{n-1} \rangle \end{equation*}

Let us rewrite $p_n\langle -, \star _{A_n} \rangle$ according to (8) and transform the above back into square form. The problem is to fill the square

Such a square is given precisely by ${\mathsf{ap}}_{\widetilde{p}_n}{({{{\mathsf{push}}}}^{(2)}{(a_0,\dots, a_{n-1})})}$ , and we are done.

Let us restate the result in a more compact and self-contained form.

For completeness, let us also state the analogous result for pointed maps.