The first statement is simply rewriting using the fact that the pullback operations f^* are given by actual pullbacks in \mathcal {C}_\mathrm {det}, and so is the local tensor product on each fiber \mathsf {Bun}_I. We also suppress the pushforwards f_!, since they simply change the morphism to the base, which is implicit in this notation anyway. Do note that these pullbacks in \mathcal {C}_\mathrm {det} are not pullbacks in \mathsf {Bun}_I!

For the second statement, by definition the set of maps from an arbitrary test object into (Y,Y,Y \times _J B) is given by \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M \times _Y Y) \times \mathsf {Bun}_I(M \times _Y B \times _J Y, A) But clearly M \times _Y Y = M, and similarly M \times _Y B \times _J Y = M \times _J B, so we can write \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M) \times \mathsf {Bun}_I(M \times _J B, A) The claim is that this is in bijection with \int ^{M \in \mathsf {Bun}_{I \times J}} \mathsf {Bun}_I(X, M \times _J Y) \times \mathsf {Bun}_I(M \times _J B, A)

We construct a bijection. Given a tuple in the first set M, \phi : X \to M, \psi : M \times _J B \to A, we carry it to M, \phi ;(1_M,p_Y), \psi , by just postcomposing the structural map to Y with Y \to J. The map p_Y is the structural map M \to Y - we form M to M \times _J Y in the obvious way and compose it with \phi . \psi , we can just leave in place.

For the other direction, given a tuple (M, \phi : X \to M \times _J Y, \psi : M \times _J B \to A), we form the tuple (M \times _J Y, \phi , \pi ;\psi ) - here we use the obvious projection \pi : M \times _J Y \times _J B \to M \times _J B.

The functoriality of these constructions makes it easy to verify that they're well-defined. Let's verify they're inverses. In one case, I start with M over J (and I), and obtain M \times _J Y. There is an obvious projection map M\times _J Y \to M, and this witnesses the equivalence of the two optics in this case. In the other case, I start with M over Y, and obtain M \times _J Y again. In this case, it's the diagonal map M \to M \times _J Y which does it.

The third statement is, again, a straightforward rewriting. The fourth statement is just a simple rewriting of the third, plus the observation that, since every object is isomorphic to one of this form, the subcategory on those is equivalent.

For the fifth statement, note that the set of ordinary optics is the set \int ^{M \in \mathcal {C}} \mathcal {C}(X, M \otimes Y) \times \mathcal {C}(M \otimes B, A)\\ \cong \int ^{M \in \mathsf {Bun}_{* \times *}}\mathsf {Bun}_*(X, M \times Y) \times \mathsf {Bun}_*(M \times B, A)\\ \cong \mathsf {FibOptic}(\mathcal {C})((*,X,A),(*,Y,B)) \cong \mathsf {FibOptic}(\mathcal {C})((X,X,X \times A),(Y,Y,Y\times A)), where the last step uses the preceding