\RequirePackage[l2tabu, orthodox]{nag}
\documentclass[10pt,fleqn,a4paper]{article}

\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{tikz}
\usepackage{tikz-cd}
\usepackage[bookmarks]{hyperref}
\usepackage{savetrees}

\newcommand{\ite}[3]{\mathbf{if}\; #1 \;\mathbf{then}\; #2
  \;\mathbf{else}\; #3}
\newcommand{\lbd}[2]{\lambda #1 \,.\, #2}
\newcommand{\fnp}[2]{\text{#1}\;(#2)}
\newcommand{\fnw}[2]{\text{#1}\;#2}
\newcommand{\fns}[2]{(\text{#1}\;#2)}
\DeclareMathOperator{\snd}{snd}
\DeclareMathOperator{\fst}{fst}
\DeclareMathOperator{\inl}{inl}
\DeclareMathOperator{\inr}{inr}
\DeclareMathOperator{\id}{id}

\title{MBProg Summary}
\date{2022-03-28}
\author{
  Florian Guthmann\\\texttt{florian.guthmann@fau.de} \and
}

\begin{document}
\maketitle{}
\section*{Semantics for Computation}
\subsection*{Evaluation Strategies}
\paragraph{$\alpha$ -conversion}
$C[\lbd{x}{t}] \to_\alpha C[\lbd{y}{t[y/x]}]$

\paragraph{$\beta$ -reduction}
$C[(\lbd{x}{t}) s] \to_\beta C(t[s/x])$

\paragraph{$\eta$ -reduction}
$C[\lbd{x}{f\,x} \to_\eta C[f]]$

\paragraph{Confluence (Church-Rosser)}
Independent reductions starting from the same term can always be joined.
\paragraph{Church Numerals}
\begin{align*}
  0 &= \lbd{f}{\lbd{z}{z}}\\
  1 &= \lbd{f}{\lbd{z}{f\,z}}\\
  2 &= \lbd{f}{\lbd{z}{f\,f\,z}}\\
\end{align*}

\subsubsection*{Standard}
We impose a \emph{left-most-outermost} evaluation order.
\paragraph{Standardization Theorem}
If $s \to_{\alpha\beta}^* t$ and $t$ is $\alpha\beta$ -normal, then $s\to_{\text{so}}^* t$ and $t$ is so-normal.

\subsubsection*{Call-by-Name (lazy)}
\paragraph{small-step}
\begin{itemize}
\item no more rewriting under $\lambda$
\item all terms are closed
\end{itemize}
\[
  \frac{}{(\lbd{x}{p}) q \to p[q/x]}\\
  \frac{p\to p'}{pq \to p'q}
\]
\paragraph{big-step}
\[
  \frac{}{\lbd{x}{p}\Downarrow \lbd{x}{p}}\\
  \frac{q\Downarrow\lbd{x}{p'} \quad p'[q/x] \Downarrow v}{pq\Downarrow v}
\]
\subsubsection*{Call-by-Value (eager)}
\paragraph{Value}
A value is a term of the form $\lbd{x}{t}$
\paragraph{small-step}
\[
  \frac{p \to p'}{pq \to p'q}\\
  \frac{q \to q' \quad p \text{ is a value}}{pq \to pq'}\\
  \frac{q \text{ is a value}}{(\lbd{x}{p}) q \to p[q/x]}
\]
\paragraph{big-step}
\[
  \frac{}{\lbd{x}{p}\Downarrow\lbd{x}{p}}\\
  \frac{p\Downarrow\lbd{x}{p'} \quad q\Downarrow q' \quad p'[q'/x]\Downarrow c}{pq\Downarrow c}
\]
\subsection*{PCF}
\paragraph{Simply-Typed Lambda-Calculus}
\[
  \text{Type} := \underbrace{A,B,C,\dots}_{\text{base types}} | \underbrace{1}_{\text{unit type}} | A \times B | A \to B
\]

$\Omega = (\lbd{x}{xx})(\lbd{x}{xx})$ is not typable.
Thus, $\to_{\alpha\beta}$ is strongly normalising for simply-typed lambda-calculus.

We obtain \emph{PCF} by:
\begin{itemize}
\item adding the fixpoint combinator $Y_A :(A\to A) \to A$ for every type $A$
\item fixing $\mathrm{Nat}$ and $\mathrm{Bool}$ as the base types
\item postulating the arithmetic and logical operations
\end{itemize}

\paragraph{Contextual Equivalence}
A term context $C$ is of \emph{ground type} if its type is either $\mathrm{Nat}$, $\mathrm{Bool}$ or $1$.
Two PCF terms $\Gamma \vdash s:A$ and $\Gamma \vdash t:A$ are \emph{contextually equivalent}, if for all contexts $C$ of ground type and for all values $v$, $C[s]\Downarrow v$ iff $C[t]\Downarrow v$
\subsubsection*{Operational Semantics}
\paragraph{Call-by-Name}
A value is
\begin{itemize}
\item a term of base or unit type
\item a pair of closed terms
\item a closed term of the form $\lbd{x}{t}$
\end{itemize}
\paragraph{Call-by-Value}
\begin{itemize}
\item a term of base or unit type
\item a pair of values
\item a closed term of the form $\lbd{x}{t}$
\end{itemize}
\subsection*{Denotational Semantics}
\paragraph{Partial Order}
A partial order $(A, \sqsubseteq)$ is a relation, such that:
\begin{itemize}
\item $a\sqsubseteq a$ (reflexivity)
\item $a \sqsubseteq b \land b \sqsubseteq c \Rightarrow a \sqsubseteq c$ (transitivity)
\item $a \sqsubseteq b \land b \sqsubseteq a \Rightarrow a = b$ (antisymmetry)
\end{itemize}
\paragraph{Complete Partial Order}
A complete partial order (pre-domain) is a partial order $(A,\sqsubseteq)$ such that for any infinite chain
\[
  a_1 \sqsubseteq a_2 \sqsubseteq \dots
\]
there is a least upper bound $a$ such that
\begin{itemize}
\item $\forall i.\; a_i\sqsubseteq a$
\item $\forall i.\; a_i \sqsubseteq b \Rightarrow a\sqsubseteq b$
\end{itemize}
We denote such a by $\bigsqcup_i a_i$

\paragraph{Domain}
A pointed cpo (\emph{domain}) is a cpo that contains an element $\bot$ such that $\forall a\in A. \bot \sqsubseteq a$

\paragraph{Monotonicity}
A function $f: A\to B$ between partial orders is \emph{monotone} if
\[
  a \sqsubseteq b \Rightarrow f(a) \sqsubseteq f(b)
\]
\paragraph{Scott-continuity}
A monotone function $f : A\to B$ between cpos is continuous if for any chain $a_1 \sqsubseteq a_2 \sqsubseteq \dots$
\[
  f\left(\bigsqcup_i a_i\right) = \bigsqcup_i f(a_i)
\]
\paragraph{Strictness}
A function $f: a\to B$ is \emph{strict} if $f(\bot) = \bot$

\paragraph{Products of Predomains}
\[
  A\times B = \{(a,b) | a\in A, b\in B\}\\
  (a_1,b_1) \sqsubseteq (a_2,b_2) \text{if} a_1 \sqsubseteq a_2 \land b_1 \sqsubseteq b_2
\]
Pairing is continuous: $\bigsqcup_i(a_i,b_i) = \left(\bigsqcup_ia_i, \bigsqcup_jb_j\right)$
\paragraph{Lifting predomains and functions}
\[
  A_\bot = A \uplus {\bot} = {(\star,a)| a\in A} \cup {(\bot,\star)}\\
  a\sqsubseteq b \text{ if } a =\bot \text{ or } a\in A,b\in A \text{ and } a\sqsubseteq b\\
\]
\[
  f^*(x) = \begin{cases}
             f(y) & \text{if } x = \lfloor y \rfloor\\
             \bot & \text{if } x = \bot
    \end{cases}
\]
  
\paragraph{Function Spaces}
Let $(A,\sqsubseteq)$, $(B,\sqsubseteq)$ be predomains.
$(A \to B,\sqsubseteq)$ is the function space predomain where:
\[
  A\to B = \{f: A\to B \mid f \text{ is continuous}\}\\
  f\sqsubseteq g \Leftrightarrow \forall x. f(x) \sqsubseteq g(x)
\]
We define:
\begin{align*}
  \text{curry} &: (A\times B \to C)\to (A\to (B \to C))\\
  \text{uncurry} &: (A\to (B \to C))\to (A \times B \to C)\\
  \text{ev} &: (A\to B) \times A \to B\\
\end{align*}
If $B$ is a domain, so is $A\to B$ with the bottom element being $\lbd{x}{\bot}$
\paragraph{Kleene`s Fixpoint Theorem}
Let f be a continuous function $f: D\to D$ over a domain $D$
\begin{itemize}
\item least fixpoint: $\exists \mu f \in D$ such that $f(\mu f) = \mu f$ and $\forall x \in D. f(x) = x \Rightarrow \mu\;f \sqsubseteq x$
\item $\mu\;f = \bigsqcup_if^i(\bot)$, where $f^0(x) = \bot, f^{i+1}(x) = f(f^i(x))$
\item least prefixpoint: $f(\mu\;f) \sqsubseteq \mu\;f$ and $\forall x \in D. f(x) \sqsubseteq x \Rightarrow \mu\;f \sqsubseteq x$
\end{itemize}
\subsubsection*{CBN}
\paragraph{Soundness}
A denotational semantics is \emph{sound} if
\[
  p\Downarrow v \Rightarrow \llbracket p \rrbracket = v
\]
\paragraph{Adequacy}
A denotational semantics is \emph{adequate} if for $p$ of ground type
\[
  \llbracket p \rrbracket = v \Rightarrow p \Downarrow v
\]
for every \emph{value} $v$
\paragraph{Compositionality}
\[
  \llbracket C[t] \rrbracket =\llbracket C \rrbracket\left[\llbracket t \rrbracket\right] 
\]

\begin{align*}
  \llbracket 1 \rrbracket &= 1_\bot\\
  \llbracket \mathrm{Nat} \rrbracket &= \mathrm{Nat}_\bot\\
  \llbracket \mathrm{Bool} \rrbracket &= \mathrm{Bool}_\bot\\
  \llbracket A\times B \rrbracket &= \llbracket A \rrbracket \times \llbracket B \rrbracket\\
  \llbracket A\to B \rrbracket &= \llbracket A \rrbracket \to \llbracket B \rrbracket\\
\end{align*}

Given a term in context $\Gamma \vdash t: A$ where $\Gamma = x_1:A_1,\dots,x_n:A_n$ the semantics $\llbracket \Gamma \vdash t:A\rrbracket$ is a continuous function $\llbracket A_1\rrbracket \times \dots \times \llbracket A_n\rrbracket \to \llbracket A \rrbracket$ ($\llbracket\dots\rrbracket_\rho = \llbracket\dots\rrbracket(\rho)$)
\begin{align*}
  \llbracket \Gamma \vdash x_i:A_i\rrbracket_\rho &= \mathrm{proj}_i(\rho)\\
  \llbracket \Gamma \vdash \star:1\rrbracket_\rho &= \lfloor \star \rfloor\\
  \vdots&\\
  \llbracket \Gamma \lbd{x}{t} : A\to B\rrbracket_\rho &= (\mathrm{curry} \llbracket\Gamma,x:A \vdash t:B\rrbracket)(\rho)\\
  \llbracket \Gamma st: B\rrbracket_\rho &= \mathrm{ev}(\llbracket\Gamma\vdash s: A\to B\rrbracket_\rho,\rrbracket\Gamma\vdash t: A\rrbracket_\rho\\
  \llbracket\Gamma \vdash Y_A\rrbracket &=\mu
\end{align*}

\subsubsection*{CBV}
\subsubsection*{Full Abstraction}
The implication $p =_{ctx} q \Rightarrow \llbracket p \rrbracket = \llbracket q \rrbracket$ is called full abstraction. It would mean that operational semantics and denotational semantics agree as far as program equivalence.
However consider the \texttt{por} function. It is not definable in PCF, but it is a continuous function and thus can be used in the denotational semantics.
\begin{align*}
  \mathtt{por}(\mathrm{True},x)       &= \mathrm{True}\\
  \mathtt{por}(x,\mathrm{True})       &= \mathrm{True}\\
  \mathtt{por}(\mathrm{False}, \mathrm{False}) &= \mathrm{False}\\
  \mathtt{por}(x,y)          &= \bot
\end{align*}
We can construct a function $t: \mathrm{Bool} \to (\mathrm{Bool} \to \mathrm{Bool} \to \mathrm{Bool}) \to \mathrm{Bool}$ in PCF that tests if a given function is $\mathtt{por}$.


\section*{Category Theory}
\paragraph{Category}
A Category $\mathcal{C}$ consist of a collection of objects $\mathrm{Ob}(\mathcal{C})$ and a collection of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$ for any $A,B \in \mathrm{Ob}(\mathcal{C})$ such that:
\begin{itemize}
\item for every $A\in \mathrm{Ob}(\mathcal{C})$ there is an \emph{identity morphism} $id_A \in \mathrm{Hom}_{\mathcal{C}}(A,A)$
\item for any $f \in \mathrm{Hom}_{\mathcal{C}}(B,C)$ and $g \in \mathrm{Hom}_{\mathcal{C}}(A,B)$ we can form a \emph{composition} $f\circ g \in \mathrm{Hom}_{\mathcal{C}}(A,C)$
\item $\id\circ f = f$ (left identity)
\item $f\circ \id = f$ (right identity)
\item $(f\circ g) \circ h = f \circ (g \circ h)$ (associativity)
\end{itemize}
\paragraph{Terminal Object}
A terminal object is an object $1\in \mathrm{Ob}(\mathcal{C})$ such that for any $A\in \mathrm{Ob}(\mathcal{C})$, there is a unique morphism $!_A : A \to 1$.

\paragraph{Initial Object}
An initial object is an object $0 \in \mathrm{Ob}(\mathcal{C})$ such that for any $A\in \mathrm{Ob}(\mathcal{C})$, there is a unique morphism $\mbox{!`}_A : 0 \to A$.

\paragraph{Isomorphism}
An \emph{isomorphism} between objects $A$ and $B$ in a category $\mathcal{C}$ is a pair of morphisms $f : A\to B,\;g : B \to A$ such that:
\[
\begin{tikzcd}
A \arrow[r, "f"] \arrow[rd, "\id_A"'] & B \arrow[d, "g"] \arrow[rd, "\id_B"] &   \\
                                     & A \arrow[r, "f"]                    & B
\end{tikzcd}
\]
\paragraph{Cartesian Category}
A \emph{cartesian category} is a category with a terminal object an binary products
                                   
\subsection*{Products and Coproducts}
\subsubsection*{Binary Products}
A product of objects $A,B$ in a category $\mathcal{C}$ is a triple $(A\times B, \fst, \snd)$ such that for any $C\in \mathrm{Ob}(\mathcal{C})$ and $f: C\to A$ and $g : C\to B$ there is a \emph{unique} morphism $\langle f,g \rangle : C \to A \times B$:
\[
\begin{tikzcd}
  & C \arrow[ld, "f"'] \arrow[rd, "g"] \arrow[d, "{\langle f,g\rangle}"', dashed] &   \\
A & A\times B \arrow[r, "\snd"'] \arrow[l, "\fst"]                & B
\end{tikzcd}
\]
\subsubsection*{Coproducts}
A coproduct of objects $A,B$ in a category $\mathcal{C}$ is a triple $(A+B, \inl, \inr)$ such that for any  $f: A\to C$ and $g : B\to C$ there is a \emph{unique} morphism $[f,g]  : A+B\to C$:
\[
\begin{tikzcd}
                                             & C                                &                                              \\
A \arrow[r, "\inl"'] \arrow[ru, "f"] & A+B \arrow[u, "{[f,g]}", dashed] & B \arrow[l, "\inr"] \arrow[lu, "g"']
\end{tikzcd}
\]
\subsection*{Functor}
A covariant Functor $F$ between categories $\mathcal{C}$ and $\mathcal{D}$ is a correspondence sending any $A\in \mathrm{Ob}(\mathcal{C})$ to $FA\in \mathrm{Ob}(\mathcal{D})$ and any $f\in \mathrm{Hom}_{\mathcal{C}}(A,B)$ to $Ff\in \mathrm{Hom}_{\mathcal{D}}(FA,FB)$ such that:
\[
  F(\id_A) = \id_{FA}\\
  F(f\circ g) = F(f) \circ F(g)
\]

\paragraph{Example: Forgetful Functor}
\[
  G: \mathrm{Cpo} \to \mathrm{Set}\\
  G(A,\sqsubseteq) = A\\
  G(f) = f
\]
\paragraph{Example: Endofunctor}
An \emph{endofunctor} is a functor from a category into itself.

\paragraph{Contravariant Functor}
A functor $F: \mathcal{C}^{\mathrm{op}} \to D$ is a contravariant functor from $\mathcal{C}$ to $\mathcal{D}$.

\paragraph{Bifunctor}
A bifunctor is a functor $\mathcal{C}\times\mathcal{D}\to \mathcal{E}$.
\subsection*{Natural Transformations}
Let $\mathcal{C}, \mathcal{D}$ be categories and $F,G : \mathcal{C} \to \mathcal{D}$ be functors.
A \emph{natural transformation} $\vartheta : F \to G$ is a family of morphisms
\[
  (\vartheta_C : FC \to GC)_{c\in \mathrm{Ob}(\mathcal{C})}
\]
such that $\forall f : C \to C'$ in $\mathcal{C}$:
\[
\begin{tikzcd}
FC \arrow[d, "\vartheta_C"] \arrow[r, "Ff"] & FC' \arrow[d, "\vartheta_{C'}"] \\
GC \arrow[r, "Gf"]                          & GC'                            
\end{tikzcd}
\]
\subsection*{Monad}
\subsubsection*{Kleisli Triple}
A \emph{Monad} in a category $\mathcal{C}$ is given by a triple $(T,\eta, -^*)$ where:
\begin{itemize}
\item $T: \mathrm{Ob}(\mathcal{C}) \to \mathrm{Ob}(\mathcal{C})$
\item unit: $\eta$ is a family $(\eta_X : X \to TX)_{x\in \mathrm{Ob}(\mathcal{C})}$
\item Kleisli lifting: for any $f : A \to TB$, $f^* : TA \to TB$
\end{itemize}
such that:
\[
  \eta^* = \id\\
  f^* \eta = f\\
  (f^*g)^* = f^*g^*
\]

\paragraph{Kleisli Category}

\subsubsection*{From Endofunctor and Natural Transformation}
A \emph{Monad} in a category $\mathcal{C}$ consists of an endofunctor $T: \mathcal{C} \to \mathcal{C}$ an natural transformations
\begin{itemize}
\item unit: $\eta : \mathrm{Id} \to T$
\item multiplication: $\mu : TT \to T$
\end{itemize}
such that:
\[
  \mu\circ\mu_T = \mu\circ T\mu \\
  \mu\circ\eta_T = \id = \mu\circ T\eta
\]
\[
\begin{tikzcd}
TTTX \arrow[r, "\mu_{TX}"] \arrow[d, "T\mu_X"] & TTX \arrow[d, "\mu_X"] &  & TX \arrow[r, "\eta_{TX}"] \arrow[rd, "\id_{TX}"'] & TTX \arrow[d, "\mu_X"] & TX \arrow[l, "T\eta_X"'] \arrow[ld, "\id_{TX}"] \\
TTX \arrow[r, "\mu_X"]                         & TX                     &  &                                                  & TX                     &                                               
\end{tikzcd}
\]
\subsection*{Tensorial Strength}
\paragraph{Cartesian Closure}
A category $\mathcal{C}$ is \emph{cartesian closed}(CCC) if it is cartesian, and for any objects $B$ and $C$ there is an object $B^C$, called an exponential, for which
\[
  \text{curry}: \mathrm{Hom}(A\times B,C) \cong \mathrm{Hom}(A, C^B)
\]
which is natural in $A$ such that
\[
\begin{tikzcd}
{\mathrm{Hom}(A\times B,C)} \arrow[rr, "\text{curry}"] \arrow[d, "{\mathrm{Hom}(f\times B,C)}"] &  & {\mathrm{Hom}(A,C^B)} \arrow[d, "{\mathrm{Hom}(f,C^B)}"] \\
{\mathrm{Hom}(A'\times B,C)} \arrow[rr, "\text{curry}"]                                &  & {\mathrm{Hom}(A',C^B)}                         
\end{tikzcd}
\]
We can generalize the CBV semantics of PCF by:
\begin{itemize}
\item replace $(-)_\bot$ with $T$
\item replace ``let'' with ``do''
\item replace $\lfloor - \rfloor$ with \texttt{return}
\end{itemize}

\paragraph{Strong Functor}
A strong Functor is a functor $F: \mathcal{C}\to\mathcal{D}$ between cartesian categories $\mathcal{C}$ and $\mathcal{D}$, plus \emph{strength}, which is a natural transformation $\tau_{A,B}:A\times FB \to F(A\times B)$ such that
\[
\begin{tikzcd}
1\times FX \arrow[rr, "\snd"] \arrow[d, "\tau"] &  & FX \\
F(1\times X) \arrow[rru, "F(\snd)"]             &  &   
\end{tikzcd}\\
\begin{tikzcd}
X\times Y \times FZ \arrow[rr, "\tau"] \arrow[d, "\mathrm{assoc}"] &                                         & F((X\times Y)\times Z) \arrow[d, "{F\,\mathrm{assoc}}"] \\
X\times(Y\times FZ) \arrow[rd, "X\times\tau"]             &                                         & F(X\times (Y\times Z))                         \\
                                                          & X\times F(Y\times Z) \arrow[ru, "\tau"] &                                               
\end{tikzcd}
\]

\subsubsection*{Strong Monads}
A monad is \emph{strong} if it is strong as a functor and $\eta,\mu$ are strong natural transformations.
\[
\begin{tikzcd}
X\times Y \arrow[r, "\eta"] \arrow[d, "\id\times\eta"'] & T(X\times Y) \\
X\times TY \arrow[ru, "\tau"']                         &             
\end{tikzcd}\\
\begin{tikzcd}
X\times TTY \arrow[rr, "\id\times\mu"] \arrow[d, "\tau"] &                                 & X\times TY \arrow[d, "\tau"] \\
T(X\times TY) \arrow[rd, "T\tau"]                       &                                 & T(X\times Y)                 \\
                                                        & TT(X\times Y) \arrow[ru, "\mu"] &                             
\end{tikzcd}
\]
\subsubsection*{Commutative Monads}
A strong monad $T$ is commutative if

\begin{tikzcd}
TA\times TB \arrow[r, "\tau"] \arrow[d, "\hat{\tau}"] & T(TA\times B) \arrow[r, "T\hat{\tau}"] & TT(A\times B) \arrow[dd, "\mu"] \\
T(A\times TB) \arrow[d, "T\tau"]                      &                                        &                                 \\
TT(A\times B) \arrow[rr, "\mu"]                       &                                        & T(A\times B)                   
\end{tikzcd}

In other words,
\[
  \text{do}\; x = p; \text{do}\; y = q; \text{return} \langle x,y\rangle == \text{do}\; y = q; \text{do}\; x = p; \text{return} \langle x,y\rangle
\]

\subsubsection*{Monoidal Categories}
A category $\mathcal{C}$ is \emph{monoidal} if there exists:
\begin{itemize}
\item a bifunctor $C \times C \to C$ (tensor product)
\item an object $I$ (unit object)
\item natural transformations
  \[
    \alpha_{A,B,C}: A \otimes (B\otimes C) \cong (A\otimes B) \otimes C\\
    \lambda_{A}: I\otimes A \cong A\\
    \rho_A:A\otimes I \cong A
  \]
\end{itemize}
A \emph{monoid} in a monoidal Category $\mathcal{C}$ is a triple $(M,\varepsilon, \odot)$ where $M$ is an object in $\mathcal{C}$, $\odot$ is a morphism $M\otimes M \to M$ and $\varepsilon$ is a morphism $I\to M$ such that:
\[
\begin{tikzcd}
M\otimes I \arrow[rd, "\rho_M"] \arrow[r, "\id_m\otimes\varepsilon"] & M\otimes M \arrow[d, "\odot"] & I\otimes M \arrow[ld, "\lambda_M"] \arrow[l, "\varepsilon\otimes \id_M"] \\
                                                                 & M                             &                                                                     
                                                               \end{tikzcd}\\
                                                               \begin{tikzcd}
M\otimes (M \otimes M) \arrow[rr, "{\alpha_{M,M,M}}"] \arrow[dd, "\id_M\otimes\odot"] &   & (M\otimes M)\otimes M \arrow[dd, "\odot\otimes \id_M"] \\
                                                                                     &   &                                                       \\
M\otimes M \arrow[r, "\odot"']                                                       & M & M\otimes M \arrow[l, "\odot"]                        
\end{tikzcd}
\]
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
