
\newcommand{\Nat}{{\mathbb N}}
\newcommand{\Real}{{\mathbb R}}
\usepackage{graphicx}
%\usepackage{amssymb}
%\usepackage{amsmath}
%\usepackage{proof}
%\usepackage{diagrams}
\newcommand{\pbe}{\mbox{ {\bf be }} }
\newcommand{\plet}{\mbox{{\bf let }} }
\newcommand{\pin}{\mbox{ {\bf in }} }
\newcommand{\por}{\mbox{ {\bf or} } }
\newcommand{\id}{{\rm id}}
\newcommand{\Cat}[1]{{\cal #1}}
\newcommand{\cat}[1]{{\mathbb #1}}
\newcommand{\Ob}[1]{{\rm ob}({\cal #1})}
\newcommand{\Hom}[1]{{\rm Hom}_{\cal #1}}
\newcommand{\Graph}[2]{( #1 \pile{\longrightarrow \\ 
\longrightarrow \\ \quad} #2)}
\newcommand{\farrow}{\longrightarrow}
\newcommand{\tensor}{\otimes}
\newcommand{\tr}[2]{\mbox{\sf tr}_{#1}(#2)}
\newcommand{\fix}[2]{\mbox{\sf fix}_{#1}#2}

%%%%%%%%%%%%%%%%%%%%% THEOREM ENVIRONMENTS %%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

%%%%%%%%%%%%%%%%%%%% DEFINITION ENVIRONMENT %%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{definition}[theorem]{Definition}

%%%%%%%%%%%%%%%%%%% REMARK AND EXAMPLES ENVIRONMENT %%%%%%%%%%%%%%%%%%%%%


\newtheorem{remark}{Remark}
\newtheorem{example}{Example}


%%%%%%%%%%%%%%%%%%%%%%%% MACROS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%  Symbols for relations %%%%%%%%%%%%%%%%%%%%%%%%%%%

% Definitional equality
\newcommand{\defeq}{=_{\mathrm{def}}}

% Isomorphism 
\newcommand{\iso}{\cong}

% Equivalence
\newcommand{\equi}{\simeq} 

% Retraction
\newcommand{\retequi}{\unlhd}

%%%%%%%%%%%% Symbols for various forms of composition %%%%%%%%%%%%%%

% Basic form of composition
\newcommand{\co}{\,}

% Kleisli composition

\newcommand{\kc}{\cdot}

% Other composition
\newcommand{\comp}{\circ}

% Species composition

\newcommand{\ks}{\circ}

%%%%%%%%%%%%%%%  Categories, 2-categories, Bicategories %%%%%%%%%%%%%

% Categories
\newcommand{\tcat}{\mathbf}

% 2-categories, bicategories
\newcommand{\bcat}{\mathcal}

% Opposite
\newcommand{\op}{\mathit{op}}

% Left adjoint, free algebras

\newcommand{\lef}{\mathcal{L}}

% Special letters for bicategories and 2-categories

\newcommand{\ba}{\bcat{A}}
\newcommand{\bc}{\bcat{C}}
\newcommand{\bl}{\bcat{L}}
\newcommand{\bx}{\bcat{X}}
\newcommand{\bk}{\bcat{K}}
\newcommand{\bsk}{\bcat{X}}
\newcommand{\bm}{\bcat{M}}
\newcommand{\bn}{\bcat{N}}
\newcommand{\bb}{\bcat{B}}
\newcommand{\bh}{\bcat{H}}
\newcommand{\bs}{\bcat{A}}
\newcommand{\be}{\bcat{A}}

\newcommand{\bbf}{\mathit{Fin}_\bk}
\newcommand{\bend}{\mathit{End}_\bk}

% Explicitly defined 2-categories

\newcommand{\myCat}{\tcat{Cat}}
\newcommand{\myCAT}{\tcat{CAT}}
\newcommand{\COC}{\tcat{COC}}
\newcommand{\FIL}{\tcat{FIL}}
\newcommand{\MONCOC}{\tcat{MONCOC}}
\newcommand{\Prof}{\tcat{Prof}}
\newcommand{\Pos}{\tcat{Pos}}
\newcommand{\Lin}{\tcat{Lin}}
\newcommand{\SProf}{S\text{-}Prof}

%%%%%%%%%%%%%%%%%%%%% Kleisli structures %%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Symbols in the definition of Kleisli structure

% Kleisli structure T 

\newcommand{\mt}{T}

% Yoneda 
\newcommand{\yo}{y}
\newcommand{\yon}{\eta}

% Sharp
\newcommand{\sh}{\sharp}
% Dagger
\newcommand{\da}{\dag}
% Double dagger
\newcommand{\dda}{\ddag}

\newcommand{\e}{\eta}
\newcommand{\et}{\eta^\mt}

% Multiplication and unit of the pseudo-monad

\newcommand{\mut}{\mu^\mt}
\newcommand{\mtt}{\mt^2}
\newcommand{\mttt}{\mt^3}

% Kleisli bicategory

\newcommand{\kl}{\mathit{Kl}}
\newcommand{\cokl}{\mathit{co}\text{-}\mathit{Kl}}

%%%%%%%%%%%%%%%%%%%%%%% Pseudo-adjunctions %%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Symbol in the definition of pseudo-adjunctions


% Counit
\newcommand{\eps}{\varepsilon}


%%%%%%%%%%%%%%%%%%%%%%%%%Up and Down sets%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\downset}{\makebox[1mm]{$\downarrow$}}
\newcommand{\upset}{\makebox[1mm]{$\uparrow$}}
\newcommand{\relmap}{\longrightarrow \hspace{-4mm}\rule{.1mm}{2mm}\quad\,}
\newcommand{\kleislimap}{\longrightarrow \hspace{-5mm}\bullet\quad\,}
%%%%%%%%%%%%%%%%%%%%%%%%%% 2-monads %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Monad S

\newcommand{\ms}{S}
\newcommand{\es}{e}
\newcommand{\mus}{m}

\newcommand{\mss}{\ms^2}
\newcommand{\msss}{\ms^3}

% Monad R 

\newcommand{\mr}{R}
\newcommand{\er}{\eta^\mt}
\newcommand{\mur}{\mu^\mr}


%%%%%%%%%%%%%%%%%%%%%%%%%%% Algebras %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Various 2-categories of algebras: S-Alg, Ps-S-Alg 

% Notation to distinguish (or not) an algebra from its underlying object.
\newcommand{\alg}{}

% S-algebras

\newcommand{\strSalg}{\ms\text{-}\mathit{Alg}_s}
\newcommand{\Salg}{\ms\text{-}\mathit{Alg}}
\newcommand{\psSalg}{\mathit{Ps}\text{-}\ms\text{-}\mathit{Alg}}

% S'-algebras

\newcommand{\Spalg}{\ms'\text{-}\mathit{Alg}}
\newcommand{\psSpalg}{\mathit{Ps}\text{-}\ms'\text{-}\mathit{Alg}}

% R-algebras

\newcommand{\strRalg}{\mr\text{-}\mathit{Alg_s}}
\newcommand{\Ralg}{\mr\text{-}\mathit{Alg}}

% Other algebras

\newcommand{\SALG}{S\text{-}\mathit{ALG}}
\newcommand{\PsSALG}{\mathit{Ps}\text{-}S\text{-}\mathit{ALG}}

% Free and forgetful functors

\newcommand{\freeF}{F}
\newcommand{\forgetU}{G}
\newcommand{\forgetG}{G}

%%%%%%%%%%%%%%%%%%%%%%%%%  Presheaves %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\psh}[1]{\mathcal{P}({#1})}

\newcommand{\pshh}{\mathcal{P}}

\newcommand{\pshA}{\psh{A}}
\newcommand{\pshB}{\psh{B}}
\newcommand{\pshC}{\psh{C}}

\newcommand{\pshSA}{\psh{SA}}
\newcommand{\pshSB}{\psh{SB}}
\newcommand{\pshSC}{\psh{SC}}


\newcommand{\Alg}[1]{\mbox{\rm $#1$-Alg}}
%%%%%%%%%%%%%%%%%%%%%%% Cocomplete categories %%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\coc}{\mathcal}
\newcommand{\cocr}{\coc{C}}
\newcommand{\cocs}{\coc{D}}

\newcommand{\coca}{\coc{A}}
\newcommand{\cocb}{\coc{B}}
\newcommand{\cocB}{\coc{B}}
\newcommand{\cocc}{\coc{C}}

%%%% Day tensor product and lifting of the presheaf Kleisli structure %%%%

\newcommand{\dayA}{\pshA}
\newcommand{\dayB}{\pshB}

\newcommand{\liftP}{\widehat{\pshh}}


%%%%%%%%%%%%%%%%%%%%%%%%  Liftings %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\liftT}{\widehat{\mt}}
\newcommand{\liftY}{\widehat{\yo}}
\newcommand{\liftDa}{\ddag}
\newcommand{\liftEta}{\widehat{\eta}}
\newcommand{\liftL}{\widehat{L}}
\newcommand{\liftI}{\widehat{I}}
%%%%%%%%%%%%%%%%%%%%%%%%%% Extensions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\extU}{\tilde{U}}
\newcommand{\extF}{\tilde{\freeF}}
\newcommand{\extS}{\tilde{S}}

\newcommand{\extEta}{\tilde{e}}
\newcommand{\extMu}{\tilde{m}}

\newcommand{\exte}{\tilde{e}}
\newcommand{\extm}{\tilde{m}}

%%%%%%%%%%%%%%%%%%%% Composite Kleisli structure %%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\mst}{\ms \mt}

%%%%%%%%%%%%%%%%% Auxiliary definitions for a diagram %%%%%%%%%%%%%%%%%%%%%

\newcommand{\myr}{(\kappa_{h, g} \, f)^\sh}
\newcommand{\myv}{\kappa_{h, g^\sh \, f}}
\newcommand{\myt}{h^\sh \, \kappa_{g, f}}
\newcommand{\myu}{\kappa_{h^\sh \, g , f}}
\newcommand{\mys}{\kappa_{h, g} \, f^\sh}

%%%%%%%%%%%%%%%%%%%%%%%% NEW MACROS FROM NICOLA %%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\fra}{(h^\sh \co g)^\sh \eta_f}
\newcommand{\frb}{\varepsilon_{(h^\sh g)^\sh \co f^\sh}}
\newcommand{\frc}{(h^\sh \co \eta_g)^\sh \co f^\sh}
\newcommand{\frd}{\varepsilon_{h^\sh \co g^\sh} \co f^\sh}
\newcommand{\fre}{h^\sh \co \varepsilon_{g^\sh \co f^\sh}}
\newcommand{\frf}{h^\sh \co (g^\sh \co \eta_f)^\sh}
\newcommand{\frg}{\varepsilon_{h^\sh \co (g^\sh \co f)^\sh}}
\newcommand{\frh}{(h^\sh \co \eta_{g^\sh \co f})^\sh}
\newcommand{\fri}{(\varepsilon_{h^\sh \co g^\sh} \co f)^\sh}
\newcommand{\frj}{((h^\sh \co \eta_g)^\sh \co f)^\sh }
\newcommand{\frmm}{((h^\sh \co g^\sh \co \yo)^\sh \co \eta_f)^\sh}
\newcommand{\frn}{\varepsilon_{(h^\sh \co g^\sh \co \yo)^\sh} \co f^\sh}
\newcommand{\fro}{(\varepsilon_{h^\sh \co g^\sh} \co f^\sh \co \yo)^\sh}
\newcommand{\frp}{\varepsilon_{h^\sh \co g^\sh \co f^\sh}}
\newcommand{\frq}{(h^\sh \co \eta_{g^\sh \co f^\sh \co \yo})}
\newcommand{\frr}{\varepsilon_{h^\sh ( g^\sh \co f^\sh \co \yo)}}
\newcommand{\frs}{(h^\sh \co (g^\sh \co \eta_f)^\sh \co \yo)}
\newcommand{\frt}{((h^\sh \co g^\sh \yo)^\sh \co \eta_f)^\sh}
\newcommand{\fru}{((h^\sh \co \eta_f)^\sh \co f^\sh \co \yo)^\sh}

