Supplementary note · AI-generated prose

Pairing and precomposition

AI-generated prose accompanying the Agda code. This note is supplementary to the book and is not part of the authors' manuscript.

This supplementary note and its code links describe the earlier formalization. Its proof explanation has not been migrated to rebuild2. Browse the current Chapter 1 code.

Read the Agda code alongside this note.Click dotted-underlined statements to read their Agda code. Browse all code.

Pairing and precomposition

The proof of pairing and precomposition reduces several calculations to the two projections of a product. This note spells out that reduction and the comparisons it must retain. All categories and functors in the statements below are absolute. We write \(\beta _1(f,g)\colon \pi _1\circ (f,g)=f\) and \(\beta _2(f,g)\colon \pi _2\circ (f,g)=g\) for the chosen projection identifications, and \[ \kappa (f,g,r)\colon (f,g)\circ r=(f\circ r,g\circ r) \] for the precomposition comparison. Vertical composition \(\delta \cdot \gamma \) applies \(\gamma \) first. The symbol \(\star \) denotes whiskering.

Supplementary Lemma 1. Let \(h,k\colon X\to C\times D\) and \(\sigma ,\tau \colon h=k\). Identifications \[ \pi _1\star \sigma =\pi _1\star \tau , \qquad \pi _2\star \sigma =\pi _2\star \tau \] give an identification \(\sigma =\tau \).

Proof idea

The product axiom gives an equivalence \[ (h=k)\longrightarrow (\pi _1\circ h=\pi _1\circ k)\times (\pi _2\circ h=\pi _2\circ k) \] whose components are the two postwhiskering functors. Pair the given identifications, using the precomposition comparison to identify the images of \(\sigma \) and \(\tau \) with their paired projections, and reflect the resulting identification through this equivalence. The conclusion is an identification between \(\sigma \) and \(\tau \), not a strict equality of expressions. □

Supplementary Lemma 2. The chosen pairing of identifications satisfies \[ (\mathrm {id}_f,\mathrm {id}_g)=\mathrm {id}_{(f,g)}, \] and, for composable identifications \(\sigma _1,\sigma _2\) and \(\tau _1,\tau _2\), \[ (\sigma _2\cdot \sigma _1,\tau _2\cdot \tau _1) =(\sigma _2,\tau _2)\cdot (\sigma _1,\tau _1). \]

Proof idea

For \(\sigma \colon f=f'\) and \(\tau \colon g=g'\), the first projection of the chosen pairing is \[ \pi _1\star (\sigma ,\tau ) =\beta _1(f',g')^{-1}\cdot \bigl (\sigma \cdot \beta _1(f,g)\bigr ). \] Thus the first projection of the identity assertion follows by cancelling \(\beta _1(f,g)\) with its inverse. For composition, substitute the displayed formula twice, reassociate, and cancel the two occurrences of the intermediate projection comparison. The result is precisely the formula for \(\sigma _2\cdot \sigma _1\). Postwhiskering preserves vertical composition, so this computes the projection of the right-hand side as well. Repeat with the second projection and apply Supplementary Lemma 1. □

Changing the inputs

Supplementary Lemma 3. Let \(f,f'\colon X\to C\), \(g,g'\colon X\to D\), and \(r,s\colon R\to X\). For identifications \(\sigma \colon f=f'\), \(\tau \colon g=g'\), and \(\gamma \colon r=s\), there is an identification \[ (\sigma \ast \gamma ,\tau \ast \gamma )\cdot \kappa (f,g,r) =\kappa (f',g',s)\cdot \bigl ((\sigma ,\tau )\ast \gamma \bigr ), \] where \(\sigma \ast \gamma =(\sigma \star s)\cdot (f\star \gamma )\) is horizontal composition.

Proof idea

First hold \(r\) fixed and vary \(f,g\). Then hold \(f,g\) fixed and vary \(r\). For either square, postcompose with a projection and then with the target projection comparison. The projection formulas for pairing and \(\kappa \) reduce the desired square to the corresponding whiskering and associator comparisons. Cancel the target comparison and use Supplementary Lemma 1.

Paste these two squares. The composition formula in Supplementary Lemma 2 combines their paired sides into \((\sigma \ast \gamma ,\tau \ast \gamma )\), and the other sides combine into the displayed horizontal composite. This argument retains the chosen \(\kappa \) at both ends. □

Successive substitution

Write \(\alpha _{r,s,f}\colon (f\circ s)\circ r=f\circ (s\circ r)\) for the associator and \(\rho _f\colon f\circ \mathrm {id}=f\) for the right unitor.

Supplementary Lemma 4. For \(f\colon X\to C\), \(g\colon X\to D\), \(s\colon R\to X\), and \(r\colon Q\to R\), the two identifications from \(((f,g)\circ s)\circ r\) to \((f\circ (s\circ r),g\circ (s\circ r))\) satisfy \[ \begin {aligned} &\kappa (f,g,s\circ r)\cdot \alpha _{r,s,(f,g)}\\ &\quad =(\alpha _{r,s,f},\alpha _{r,s,g})\cdot \bigl (\kappa (f\circ s,g\circ s,r)\cdot (\kappa (f,g,s)\star r)\bigr ). \end {aligned} \] For the identity substitution one has \[ (\rho _f,\rho _g)\cdot \kappa (f,g,\mathrm {id})=\rho _{(f,g)}. \]

Proof idea

Project the two substitution paths. The projection formulas for \(\kappa \) leave the same projection comparison, transported through two different strings of associators. The pentagon identifies those strings. After cancelling the common comparison, apply Supplementary Lemma 1.

The identity case uses the compatibility of the right unitor with a composite: \[ \rho _{\pi \circ h} =(\pi \star \rho _h)\cdot \alpha _{\mathrm {id},h,\pi }. \] This compatibility follows from the pentagon and triangle, followed by cancellation after prewhiskering by the identity. Insert it into each projected identity square, cancel its projection comparisons, and again reflect through the product equivalence. □

These are comparisons for the specified pairing and substitution operations. They do not replace those operations by strictly associative or strictly unital ones.

Checked declarations

The linked Agda declarations were type-checked in the displayed edition. The explanatory prose and proof ideas are AI-generated and are not verified by that check.