# Categories of Optics

## Lenses

data Store s a = Store (s -> a) s

instance Functor (Store s) where
    fmap ???

get :: s -> a

put :: (s, a) -> s == s -> a -> s -- For sure by the prod-exp adjunction
put = 

get . put :: (s, a) -> a
get . put = snd

Example:

data Rectangle = R { height :: Int, width :: Int }
data Panel = P { topFace :: Rectangle, leftFace :: Rectangle, 
                 rightFace :: Rectangle, botFace :: Rectangle }

getWidth :: Rectangle -> Int
getWidth = width

getTopFace :: Panel -> Rectangle
getTopFace = topFace

putTopFace :: Panel -> Rectangle -> Panel
putTopFace (P tf lf rf bf) face = P face lf rf bf

putWidth :: Rectangle -> Int -> Rectangle
putWidth (R a b) side = R a side

putTopFaceWidth :: (Panel -> Int) -> Panel
putTopFaceWidth panel side
    = putTopFace panel (putWidth (getTopFace panel) side)
    
putTopFaceWidth ==
    -- assuming prod-exp adj
    putTopFace . 
        prodMap id putWidth . 
            prodMap (dupMap id getTopFace) id ? 
    where dupMap f g x = (f x, g x)

--Checking...
dupMap id getTopFace :: Panel -> (Panel, Rectangle) 
-- Right idea, but wrong type

prodMap (dupMap id getTopFace) id $ (panel, side)
 == (panel, topFace panel, side)
prodMap id putWidth $ (panel, topFace panel, side)
 == (panel, newTopFace)
     -- assuming (a, (b, c)) == (a, b, c)
putTopFace (panel, newTopFace)
    == newPanel

--Because
putTopFaceWidth :: (Panel, Int) -> (Panel, Rectangle, Int) -> (Panel, Rectangle) -> Panel 

-- Therefore
putTopFaceWidth = curry putTopFace . johnnyMap id putWidth . lisaMap id getTopFace id where 
    lisaMap f g h (a0, b0) = (f a0, g a0, h b0)
    johnnyMap f g (a0, b0, c0) = (f a0, g b0 c0)
    
    
--Adjunctifying...
putTopFaceWidth :: (Panel -> Int) -> (Panel -> Rectangle -> Int) -> (Panel -> Rectangle) -> Panel 

putTopFaceWidth = dupMap id getTopFace  

## Optics

$$O = \mathbf{Optic}_\mathbf{C}((S,S'), (A,A')) := \int^{M \in \mathbf{C}} \mathbf{C}(S, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right)$$

From the product-exponential adjunction and switcheroo:
\begin{align}
\mathbf{Set}\left(\mathbf{Optic}_\mathbf{C}((S,S'), (A,A')), K\right) & = \int_{M \in \mathbf{C}}\mathbf{Set}\left(\mathbf{C}(S, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right), K \right) \\
& = \int_{M \in \mathbf{C}}\mathbf{Set}\left(\mathbf{C}(M \otimes A^{\prime}, S^{\prime}),~\mathbf{Set}(\mathbf{C}\left(S, M \otimes A\right), K)\right) \\
& \cong \operatorname{Nat}\left( \mathbf{C}(- \otimes A^{\prime}, S^{\prime}),~\mathbf{Set}(\mathbf{C}\left(S, - \otimes A\right), K) \right)
\end{align}

Let $K = \{0, 1\}$, then $\mathbf{Set}(-, K) \cong P(-)$, the power-set functor. For this case,
$$P(O) \cong \operatorname{Nat}\left(\mathbf{C}(- \otimes A', S'),\ P(\mathbf{C}(S, -\otimes A))\right)$$

Let $h \in \mathbf{Set}\left(\mathbf{Optic}_\mathbf{C}((S,S'), (A,A')), K \right)$

\begin{align}
l \in \mathbf{C}(S, M \otimes A), &\ r \in \mathbf{C}(M \otimes A', S') \\
\phi_M \colon \mathbf{C}(M \otimes A', S') & \to (\mathbf{C}(S, M \otimes A) \to K) \\
\phi_M & = \pi_M(h) \\
\phi_M(r) & = \lambda l.
\end{align}

<!-- ```
? ---i_m----→ e
\ |
αₘ πₘ
\ ↓
Nat( \mathbf{C}(M ⊗ A', S'), Set(\mathbf{C}(S, M ⊗ A), K) )

e = Set(Optic_\mathbf{C}((S, S'), (A, A'), K)

---
_Optics as a Left Kan extension_

Let $K = - \otimes A'$, $D = \mathbf{C}(S, - \otimes A)$.
$$\mathbf{Lan}_K D(S') = \int^{M \in \mathbf{C}} D(M) \times \mathbf{C}(K(M), S') = \mathbf{Optic}_\mathbf{C}((S,S'), (A,A'))$$

---

\begin{align} 
l \in \mathbf{C}(S, M \otimes A), &\ r \in \mathbf{C}(N \otimes A', S') \\
f \colon M \to N \implies & \\
f \otimes A \colon M \otimes A & \to N \otimes A \\
f \otimes A' \colon M \otimes A' & \to N \otimes A' \\
(f \otimes A)l \colon S & \to N \otimes A \\
r (f \otimes A) \colon M \otimes A' & \to S'
\end{align}

Rewriting anew for $f \colon M \to N$:
\begin{align}
\stackrel{l\colon S \to M \otimes A}{\mathbf{C}(S, M \otimes A)} & \stackrel{C(S, f \otimes A)}{\longrightarrow} \quad \stackrel{(f \otimes A) l\colon S \to N \otimes A}{\mathbf{C}(S, N\otimes A)}\\
\stackrel{r\colon N \otimes A' \to S'}{\mathbf{C}(N \otimes A', S')} & \stackrel{C(f \otimes A', S')}{\longrightarrow} \quad \stackrel{r(f \otimes A') \colon M \otimes A' \to S'}{\mathbf{C}(M\otimes A', S')}\\
\end{align}

Now:
\begin{align}
P(M, N) = {\mathbf{C}(S, M \otimes A)} \times \mathbf{C}(N \otimes A', S')\\
P(M, N) \stackrel {P(f, id_N)} \longrightarrow P(N, N) \to \coprod_{K \in \mathbf C} P(K, K) \\
P(M, N) \stackrel {P(id_M, f)} \longrightarrow P(M, M) \to \coprod_{K \in \mathbf C} P(K, K)
\end{align}

Bra-ket notation:
$$\langle y|A|x\rangle = \langle y|Ax \rangle = \langle yA^\dagger|x\rangle$$
$$ \langle y|x \rangle = \langle yA|Ax \rangle \Leftarrow A^\dagger = A^{-1}$$

$$\langle l|r \rangle = \left\langle \left(f \otimes A \right)l|r\left(f^{-1} \otimes A\right) \right\rangle$$

#### Composition of optics:

Fubini theorem:

$$ \int^{C \in \mathbf{C}} \int^{D \in \mathbf{D}} F(C, C, D, D) \cong \int^{(C, D) \in \mathbf{C} \times \mathbf{D}} F(C, C, D, D) \cong \int^{D \in \mathbf{D}} \int^{C \in \mathbf{C}} F(C, C, D, D)$$

Begin:

$$ \int^{M \in  \mathbf{C}} \mathbf{C}(S, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right) \times \int^{N \in  \mathbf{C}} \mathbf{C}(R, N \otimes S) \times \mathbf{C}\left(N \otimes S^{\prime}, R^{\prime}\right) \\
\to \int^{M \in  \mathbf{C}} \mathbf{C}(R, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, R^{\prime}\right)$$

1. $$ \int^{M \in  \mathbf{C}} \mathbf{C}(S, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right) \times \int^{N \in  \mathbf{C}} \mathbf{C}(R, N \otimes S) \times \mathbf{C}\left(N \otimes S^{\prime}, R^{\prime}\right) \\
= \int^{(M, N) \in  \mathbf{C \times C}} \mathbf{C}(S, M \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right) \times  \mathbf{C}(R, N \otimes S) \times \mathbf{C}\left(N \otimes S^{\prime}, R^{\prime}\right)$$

2. $$ \left[\mathbf{C}(S, -_1 \otimes A) \times \mathbf{C}\left(-_2 \otimes A^{\prime}, S^{\prime}\right)\right] \circ \left[\mathbf{C}(R, -_1 \otimes S) \times \mathbf{C}\left(-_2 \otimes S^{\prime}, R^{\prime}\right)\right] \\
% Incorrect = \mathbf{C}(R, -_1 \otimes A) \times \mathbf{C}\left(-_2 \otimes A^{\prime}, R^{\prime}\right) \\
= \int^{N \in \mathbf C} \left[\mathbf{C}(S, N \otimes A) \times \mathbf{C}\left(-_1 \otimes A^{\prime}, S^{\prime}\right)\right] \times \left[\mathbf{C}(R, -_2 \otimes S) \times \mathbf{C}\left(N \otimes S^{\prime}, R^{\prime}\right)\right] $$ 

3. Integrating 2. over $\forall \ M \in \mathbf C$:
    $$ \int^{M \in \mathbf C} \int^{N \in \mathbf C} \left[\mathbf{C}(S, N \otimes A) \times \mathbf{C}\left(M \otimes A^{\prime}, S^{\prime}\right)\right] \times \left[\mathbf{C}(R, M \otimes S) \times \mathbf{C}\left(N \otimes S^{\prime}, R^{\prime}\right)\right] $$
    

---

Kleisli construction of $\mathbf{Optic}_\mathbf C$ as a monad over $\mathbf C \in \mathbf{Prof}$

$\require{AMScd}$
\begin{CD}
A @<<< B @>>> C\\ 
@. @| @AAA\\ @. D @= E 
\end{CD}