This supplementary note describes an earlier formalization. Its code links are temporarily disabled pending review for rebuild2.
Constant diagrams and the exponential law
The proof that functor categories with groupoid target are groupoids uses compatibility of the exponential law with constant diagrams. We describe the comparison of the actual functors and the product calculation giving it.
For absolute categories \(T,X\), let \(\Delta _T^X\colon X\to \Fun (T,X)\) be the curry of \(\pi _1\colon X\times T\to X\). Write \[ E_{T,C,X}\colon \Fun (T,\Fun (C,X))\longrightarrow \Fun (T\times C,X) \] for the chosen exponential equivalence. The first three statements use the Chapter 1 mapping-anima and functor-category structure.
Supplementary Lemma 1. For \(F\colon C\to D\), one has an identification of functors \[ \Fun (T,F)\circ \Delta _T^C=\Delta _T^D\circ F. \]
Proof idea
Uncurry both sides. For the left side, postcomposition compatibility and the currying computation comparison identify the result with \(F\pi _1\). For the right side, restriction compatibility gives \(\pi _1(F\times \mathrm {id}_T)\), which the product projection comparison also identifies with \(F\pi _1\). Reflect through uncurrying. □
Supplementary Lemma 2. Put \(N=\Fun (C,X)\) and let \(\sigma \colon C\times T\to T\times C\) exchange the factors. The following functors \(N\to \Fun (C\times T,X)\) are identified: \[ \sigma ^*\circ E_{T,C,X}\circ \Delta _T^N =E_{C,T,X}\circ \Fun (C,\Delta _T^X). \]
Proof idea
Uncurry once. Both functors become evaluation \(N\times C\to X\) precomposed with a functor \(N\times (C\times T)\to N\times C\). For the left side, exchange \(C,T\), reassociate to \((N\times T)\times C\), and forget \(T\). For the right side, reassociate to \((N\times C)\times T\) and forget \(T\).
Compute their projections using the product comparisons. In both cases, the first projection is \(\pi _1\) and the second is \(\pi _1\pi _2\) on \(N\times (C\times T)\). The product universal property compares the two argument functors. Postcompose with evaluation and reflect through uncurrying. □
Supplementary Corollary 3. If \(\Delta _T^X\) is an equivalence, then so is \(\Delta _T^{\Fun (C,X)}\).
Proof idea
Postcomposition \(\Fun (C,\Delta _T^X)\) is an equivalence, as are both exponential functors and precomposition by \(\sigma \). Use Supplementary Lemma 2 and cancel these equivalences. For \(T=[1]\), this is the comparison used in the closure of groupoids under functor categories. □
The coproduct comparison
The following calculation is used in Section 2.5. We work in that section’s setup, including coproducts. Its linked Agda module also carries the Rezk and recognition assumptions needed for the subsequent closure results. The calculation itself uses naturality and the coproduct universal property.
Supplementary Lemma 4. Put \(d_C=\Delta _{[1]}^C\colon C\to \operatorname {Ar}(C)\), and let \(i_C,i_D\) be the inclusions into \(C\amalg D\). For the comparison \[ q=[\operatorname {Ar}(i_C),\operatorname {Ar}(i_D)]\colon \operatorname {Ar}(C)\amalg \operatorname {Ar}(D)\to \operatorname {Ar}(C\amalg D), \] there is an identification \[ q\circ (d_C\amalg d_D)=d_{C\amalg D}. \]
Proof idea
Restrict the left side to each summand. The copairing computation and precomposition comparisons give \(\operatorname {Ar}(i_C)d_C\) and \(\operatorname {Ar}(i_D)d_D\). By Supplementary Lemma 1, these identify with \(d_{C\amalg D}i_C\) and \(d_{C\amalg D}i_D\). The coproduct universal property assembles the two comparisons into the displayed identification. This computes the specific factorization used in the closure argument. □