Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.
Relative currying and evaluation
The mapping-anima definition of a dependent product gives an equivalence. To use it in calculations with actual functors over a base, one must identify its value on the names of those functors. That is the subject of this note. We use the Chapter 1 structures and the comparison convention of Triangles over a base.
Fix \(p\colon S\to T\), \(f\colon C\to S\) and a chosen dependent product \(\Pi C\to T\), with evaluation \(\varepsilon _C\colon p^*(\Pi C)\to C\) over \(S\). For \(t\colon E\to T\), denote the defining equivalence by \[ U_t\colon \Map _T(E,\Pi C)\iso \Map _S(p^*E,C). \] For a functor \(u\colon E\to \Pi C\) over \(T\), write \(\operatorname {ev}(u)=\varepsilon _Cp^*u\), with its pasted triangle over \(S\). Only the displayed dependent products are assumed to exist.
Supplementary Lemma 1. There is an identification \[ U_t(\ulcorner u\urcorner )=\ulcorner \operatorname {ev}(u)\urcorner \] in the relative mapping anima.
Proof idea
The actual functor \(U_t\) is the composite of base change on relative mapping animae with postcomposition by \(\varepsilon _C\). Base change on a named triangle names the pullback lift together with its second-projection triangle. Postcomposition on a named triangle names the pasted composite. Combine these two computations and the associator. The resulting equality is in the relative mapping anima, so the base triangle is retained throughout. □
Supplementary Lemma 2. Every functor \(w\colon p^*E\to C\) over \(S\) has a transpose \(\lambda w\colon E\to \Pi C\) over \(T\) with a comparison \(\operatorname {ev}(\lambda w)\simeq _S w\). A comparison \(\operatorname {ev}(u)\simeq _S\operatorname {ev}(v)\) induces a comparison \(u\simeq _T v\).
Proof idea
Lift the name of \(w\) through \(U_t\), and decode the resulting point to a triangle. The naming roundtrip and Supplementary Lemma 1 identify the name of its evaluation with the name of \(w\). Convert that identification to a comparison of triangles.
For reflection, name the given comparison, use Supplementary Lemma 1 at both endpoints, and reflect through \(U_t\). Decoding gives a comparison over \(T\). This asserts the existence of that comparison; it does not prescribe its image as higher comparison data under a separately chosen evaluation action. The named evaluation computation used in both arguments is proved in Supplementary Lemma 1. □
Supplementary Lemma 3. Given chosen dependent products for categories \(C,D\) over \(S\) and a functor \(a\colon C\to D\) over \(S\), put \(\Pi a=\lambda (a\varepsilon _C)\). There is a comparison \[ \varepsilon _Dp^*(\Pi a)\simeq _S a\varepsilon _C. \] The induced functors satisfy \(\Pi (\operatorname {id})\simeq _T\operatorname {id}\) and, whenever the three required dependent products are supplied, \((\Pi b)(\Pi a)\simeq _T\Pi (ba)\).
Proof idea
The evaluation comparison is the transposition computation of Supplementary Lemma 2. For the identity law, compare both evaluations with \(\varepsilon _C\), using the base-change identity comparison and the unit laws over the base, and reflect.
For composition, evaluation of a composite is compared with the evaluation of its second factor after base change of its first. This uses the base-change composition comparison, including its base triangle. Apply the two evaluation comparisons, reassociate over \(S\), and obtain \((ba)\varepsilon _C\). Reflection now gives the composition comparison over \(T\). These are the stated identity and composition comparisons, without an assertion of additional higher coherence. □