Dependent Optics and Indexed Bidirectional Structure

Proof. An object of $\mathcal{C}/A$ over $A$ is a family; $X$ is the family $B$ and $X^{\prime }$ is $B^{\prime }$. A map $X\to Y$ in $\mathcal{C}/A$ with $Y$ the terminal object of the slice is unique, so $l$ carries no information beyond the existence of $\mathsf{get}$, which is the structure map of $X$. A map $Y^{\prime }\to X^{\prime }$ in $\mathcal{C}/A$ is a section of $X^{\prime }$, that is a choice of element of $B^{\prime }(a)$ for each $a$, and that is exactly the second component of $\mathsf{put}$ once the first argument has been discarded. ◻

Proof. Proof idea. The composite is written with an explicit representative $g\circ f$; well-definedness is extranaturality of the formula in $f$ and $g$, and each law is the corresponding coherence law of a pseudofunctor, transported across (170.1).

Well-definedness. Replace the representative of the second optic by one related through $m:g\Rightarrow g_1$. Both $f^{\ast }$ and $f^{{\ast }^{\prime }}$ are functors, so the composite changes by $f^{\ast }(\mathcal{L}(m))$ on the left and $f^{{\ast }^{\prime }}(\mathcal{R}(m))$ on the right, and pseudofunctoriality identifies those with $\mathcal{L}(f\ast m)$ and $\mathcal{R}(f\ast m)$ for the whiskered $2$-morphism $f\ast m$; then (170.1) at $f\ast m$ identifies the two composites. Replacing the representative of the first optic is the same argument with the whiskering on the other side.

Unit law. Let $⟨l\mid r⟩$ have representative $f$. Then the last step because the composite $({\theta }_{{\mathrm{id}}_A,f}{)}_Y\circ ({\theta }_A{)}_{f^{\ast }Y}$ is the identity by the left unit coherence law of the pseudofunctor $\mathcal{L}$, and dually on the right; the omitted backward components are the mirror calculation with ${\theta }^{\prime }$. The other unit law uses the right unit coherence.

Associativity. Choose representatives $f,g,h$ of three optics simultaneously, which is legitimate because the coend over $\mathcal{B}(A,B)\times \mathcal{B}(B,C)\times \mathcal{B}(C,D)$ may be computed one factor at a time. Both bracketings produce the pair whose forward component is $$({\theta }_{f,h\circ g}{)}_W\circ f^{\ast }(({\theta }_{g,h}{)}_W\circ g^{\ast }(l_3)\circ l_2)\circ l_1,$$ and the associativity coherence of $\mathcal{L}$ identifies the two ways of reassociating the $\theta$’s; the backward components are the same calculation for $\mathcal{R}$, and (170.1) at the resulting isomorphism of representatives identifies the two classes. ◻

Proof. An action $\mathcal{M}\to [\mathcal{C},\mathcal{C}]$ is the same as a pseudofunctor out of the delooping, by definition 169.13: the unit and associativity data of the action are the coherence isomorphisms ${\theta }_{\ast }$ and ${\theta }_{f,g}$. With one object, $\mathcal{B}(A,B)=\mathcal{M}$ for the unique pair, so the coend of definition 170.4 is the coend of definition 169.16 with $\mathcal{C}$ split into the two categories, which is the definition of a mixed optic recalled in example 169.35. The composition formulas agree because ${\theta }_{f,g}$ is the associativity datum of the action. ◻

Proof. An object of ${\mathrm{Optic}}_{\bullet ,\mathcal{R}}$ is a triple $(X,X^{\prime }{)}_A$ with $X$ the unique object of ${\bullet }_A$, hence a pair $(A,X^{\prime })$ with $X^{\prime }\in {\mathcal{R}}_A$: the objects of the Grothendieck construction. A $1$-category has only identity $2$-morphisms, so (170.1) is the identity relation and the coend of definition 170.4 is a coproduct: $${\int }^{f\in \mathcal{B}(A,B)}{\mathcal{R}}_A(f^{{\ast }^{\prime }}{Y}^{\prime },X^{\prime })\cong \coprod _{f\in \mathcal{B}(A,B)}{\mathcal{R}}_A(f^{{\ast }^{\prime }}{Y}^{\prime },X^{\prime }),$$ which is the hom-set of the Grothendieck construction on the pointwise opposite: a morphism is a map $f$ of the base together with a map $f^{{\ast }^{\prime }}{Y}^{\prime }\to X^{\prime }$ in the fibre. Composition of definition 170.5 reduces to the composition there, since the forward components are identities and the $\theta$’s are the coherence data of the fibration. ◻

Proof. Unfold definition 170.4 for this indexed category: The first step is the universal property of the pullback; the second uses that coends commute with products; the third is lemma 169.12. In detail, the first splits a map into $M{\times }_{B}Y$ over $A$ into its component into $M$ over $A\times B$ and its component into $Y$ over $B$, the latter being the index of the product. The last step is Yoneda reduction in $M$, which substitutes $X$ for $M$. ◻

Proof. Let $A=\coprod _i{A}_i$. For every $B$, so $A$ has the universal property of the coproduct in ${\mathrm{Span}}_{\mathcal{C}}$. ◻

Proof. Let $(X_i,X_i^{\prime }{)}_{A_i}$ be a finite family. Put $A:=\coprod _i{A}_i$. By hypothesis ${\mathcal{L}}_A\cong \prod _i{\mathcal{L}}_{A_i}$ and likewise for $\mathcal{R}$, so the families $(X_i)$ and $(X_i^{\prime })$ assemble into single objects $X$ of ${\mathcal{L}}_A$ and $X^{\prime }$ of ${\mathcal{R}}_A$. A morphism $(X,X^{\prime }{)}_A\to (Y,Y^{\prime }{)}_B$ is, by definition 170.4 and the hypothesis, a family of morphisms $(X_i,X_i^{\prime }{)}_{A_i}\to (Y,Y^{\prime }{)}_B$, since $\mathcal{B}(A,B)\cong \prod _i\mathcal{B}(A_i,B)$ and the coend of a product over a product of indices is the product of the coends. That is the universal property of the coproduct.

For the particular case, lemma 170.13 gives coproducts in ${\mathrm{Span}}_{\mathcal{C}}$, and $\mathcal{C}/-$ turns them into products because $\mathcal{C}/\coprod _i{A}_i\cong \prod _i\mathcal{C}/A_i$ in a lextensive category. ◻

Proof. Proof idea. Extranaturality of ${\zeta }_f$ in $f$ is exactly the condition needed to descend a family of maps along the coend of definition 170.4, and the two coherence equations of definition 170.15 are exactly preservation of identity and composition for the descended functor.

From a representation to a functor. Given $(P,\zeta )$, define $\tilde{P}$ on objects by $\tilde{P}((X,X^{\prime }{)}_A):=P_A(X,X^{\prime })$. On morphisms, consider This is extranatural in $f$ by the hypothesis on $\zeta$, so by proposition 169.11 it descends to the coend, giving $\tilde{P}$ on hom-sets. The first equation of definition 170.15 makes $\tilde{P}$ preserve identities and the second makes it preserve composition, by comparison with definition 170.5.

The two constructions are inverse. On objects, $(\tilde{P}\circ {\iota }^{\mathrm{op}}{)}_A(X,X^{\prime })=\tilde{P}((X,X^{\prime }{)}_A)=P_A(X,X^{\prime })$. On morphisms, ${\iota }_A(l,r)$ has representative ${\mathrm{id}}_A$, so applying $\tilde{P}$ to it gives $P_A(l,r)\circ {\zeta }_{{\mathrm{id}}_A}$, which is $P_A(l,r)$ by the first equation of definition 170.15. Conversely, a functor $F$ out of ${\mathrm{Optic}}^{\mathrm{op}}$ is determined by its values on the optics ${\iota }_A(l,r)$ and on the optics $⟨\theta \mid {\theta }^{\prime -1}⟩$ of each representative, because every optic factors as one of the latter followed by one of the former; that factorization is the composition formula of definition 170.5 with $l_2$ and $r_2$ the coherence maps. ◻

Proof. By theorem 170.17 at $\mathcal{D}:=\mathbf{Set}$, the category ${\mathrm{Tamb}}_{\mathbf{Set}}$ is isomorphic to the category of presheaves on ${\mathrm{Optic}}_{\mathcal{L},\mathcal{R}}$. For any category $\mathcal{E}$ and objects $S,T$, the Yoneda lemma gives $$\mathcal{E}(S,T)\stackrel{Yoneda}{=}\mathcal{E}(-,T)(S)\stackrel{Yoneda}{=}{\int }_{F\in \hat{\mathcal{E}}}\mathbf{Set}(F(T),F(S)),$$ the second step because $\hat{\mathcal{E}}(\mathcal{E}(-,T),F)\cong F(T)$. Apply this with $\mathcal{E}:={\mathrm{Optic}}_{\mathcal{L},\mathcal{R}}$, $S:=(X,X^{\prime }{)}_A$ and $T:=(Y,Y^{\prime }{)}_B$, and transport along the isomorphism of theorem 170.17. ◻