% !TeX spellcheck = \documentclass[12pt,a4paper,italian]{book} \usepackage{graphicx} % Required for inserting images \usepackage{amssymb} %to augment generic LaTeX; needed for \mathbb font \usepackage{amsfonts} %reading in some AMS fonts \usepackage{amsthm} \usepackage{amsmath} %needed for \begin{align}... \end{align} environment \usepackage{amsxtra} \usepackage{tikz} \usepackage{tikz-cd} \usepackage{quiver} \theoremstyle{definition} \newtheorem{definition}{Definition}[section] \newtheorem{proposition}[definition]{Proposition} \newtheorem{theorem}[definition]{Theorem} \newtheorem{lemma}[definition]{Lemma} \newtheorem{corollary}[definition]{Corollary} \newtheorem*{idea}{Idea} \theoremstyle{remark} \newtheorem{remark}[definition]{Remark} \title{Tesi} \author{saladinoflavio } \date{March 2026} \usepackage{biblatex} \bibliography{Bibliografia.bib} \begin{document} \maketitle \section{Introduction} \section{Freyd cover of a category} \begin{definition}[Comma Category] Let $\mathcal{A,B,C}$ locally small categories and let $F: \mathcal{A} \to \mathcal{C}, G: \mathcal{B} \to \mathcal{C}$ two functors % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhjYWx7QX0iXSxbMiwwLCJcXG1hdGhjYWx7Q30iXSxbNCwwLCJcXG1hdGhjYWx7Qn0iXSxbMCwxXSxbMiwxXV0= \[\begin{tikzcd} {\mathcal{A}} && {\mathcal{C}} && {\mathcal{B}} \arrow[from=1-1, to=1-3] \arrow[from=1-5, to=1-3] \end{tikzcd}\] Then we call comma category of F and G \footnote{the name "comma category" arises from the notation (F,G) used by Lawvere}, $(F \downarrow G)$, the category with: \begin{itemize} \item{Objects}: an object is a triple $(A,B,f)$ where $f: F(A) \to F(B)$ is a $\mathcal{C}$-morhpism \item{Arrows}: a morphism from $(A,B,f)$ to $(A',B',f')$ is a pair $(h,k)$ of an $\mathcal{A}$-morphism $h: A \to A'$ and a $\mathcal{B}$-morphism $k: B \to B'$ such that the following diagram is commutative : % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGKEEpIl0sWzIsMCwiRyhCKSJdLFswLDIsIkYoQScpIl0sWzIsMiwiRyhCJykiXSxbMCwxLCJmIl0sWzIsMywiZiciLDJdLFsxLDMsIkcoaykiXSxbMCwyLCJGKGgpIiwyXV0= \[\begin{tikzcd} {F(A)} && {G(B)} \\ \\ {F(A')} && {G(B')} \arrow["f", from=1-1, to=1-3] \arrow["{F(h)}"', from=1-1, to=3-1] \arrow["{G(k)}", from=1-3, to=3-3] \arrow["{f'}"', from=3-1, to=3-3] \end{tikzcd}\] \end{itemize} \end{definition} \begin{remark} Notice that there are two canonical forgetful functors defined over the comma category: \begin{itemize} \item a functor $\Pi_1 : (F \downarrow G) \to \mathcal{A}$ that forget the comma structure preserving the "$\mathcal{A}$-structure" defined as: % https://q.uiver.app/#q=WzAsNixbMCwxLCIoQSxCLGYpIl0sWzAsMywiKEEnLEInLGYnKSJdLFsyLDEsIkEiXSxbMiwzLCJBJyJdLFswLDAsIihGXFxkb3duYXJyb3cgRykiXSxbMiwwLCJcXG1hdGhjYWx7QX0iXSxbMCwxLCIoaCxrKSIsMl0sWzIsMywiaCJdLFs0LDVdLFs2LDcsIiIsMix7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d \[\begin{tikzcd} {(F\downarrow G)} && {\mathcal{A}} \\ {(A,B,f)} && A \\ \\ {(A',B',f')} && {A'} \arrow["{\Pi_1}", from=1-1, to=1-3] \arrow[""{name=0, anchor=center, inner sep=0}, "{(h,k)}"', from=2-1, to=4-1] \arrow[""{name=1, anchor=center, inner sep=0}, "h", from=2-3, to=4-3] \arrow[between={0.2}{0.8}, maps to, from=0, to=1] \end{tikzcd}\] \item a functor $\Pi_2 : (F \downarrow G) \to \mathcal{B}$ (preserving the "$\mathcal{B}$-structure") defined as: % https://q.uiver.app/#q=WzAsNixbMCwxLCIoQSxCLGYpIl0sWzAsMywiKEEnLEInLGYnKSJdLFsyLDEsIkIiXSxbMiwzLCJCJyJdLFswLDAsIihGXFxkb3duYXJyb3cgRykiXSxbMiwwLCJcXG1hdGhjYWx7Qn0iXSxbMCwxLCIoaCxrKSIsMl0sWzIsMywiayJdLFs0LDUsIlxcUGlfMiJdLFs2LDcsIiIsMix7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d \[\begin{tikzcd} {(F\downarrow G)} && {\mathcal{B}} \\ {(A,B,f)} && B \\ \\ {(A',B',f')} && {B'} \arrow["{\Pi_2}", from=1-1, to=1-3] \arrow[""{name=0, anchor=center, inner sep=0}, "{(h,k)}"', from=2-1, to=4-1] \arrow[""{name=1, anchor=center, inner sep=0}, "k", from=2-3, to=4-3] \arrow[between={0.2}{0.8}, maps to, from=0, to=1] \end{tikzcd}\] \end{itemize} \end{remark} \begin{theorem}\label{completenesscomma} Let $\mathcal{A}$ and $\mathcal{B}$ be two finitely cocomplete categories and let $F:\mathcal{A} \to \mathcal{C}$, $\mathcal{B} \to \mathcal{C}$ two functors. If $F$ is a cocontinous functor - i.e. preserves small colimits - then the comma category $(F\downarrow G)$ is finitely cocomplete; morover the forgetful functors are cocontinous. \\ Analogously if $\mathcal{A}$ and $\mathcal{B}$ are finitely complete categories and $G: \mathcal{A} \to \mathcal{C}$ is continous - i.e. preserves small limits - then $(F \downarrow G)$ is finitely complete and both forgetfoul functors are continous. \end{theorem} \begin{proof} Let's begin by proving the cocomplete case. We will start from cocompleteness of the category and then we will move on to che cocontinuity of the forgetful functors. Recall that a a category is finitely cocomplete if and only if it admits initial object and pushouts; we will construct explicitely both objects: \\ \textbf{Initial Object}: We will construct the initial object of $(F, \downarrow G)$ by using the cocompletens of $\mathcal{A}$ and $\mathcal{B}$: indeed, let $0_\mathcal{A}$ be the initial object of $\mathcal{A}$ and $0_\mathcal{B}$ the initial object of $\mathcal{B}$. Now, since $F$ is a cocontinous functor $F(0_\mathcal{A}) = 0_\mathcal{C}$ where $0_\mathcal{C}$ is in $\mathcal{C}$; thus there is a unique morphism $in: F(0_\mathcal{A})=0_\mathcal{C} \to G(0_\mathcal{B})$ in $\mathcal{C}$. Now, we claim $(0_\mathcal{A},0_\mathcal{B},in)$ to be initial in $(F\downarrow G)$: \begin{itemize} \item existence: let $(A,B,f)$ be an object of $(F\downarrow G)$; then there exists two unique morphisms $in_A, in_B$ respectively in $\mathcal{A}$ and $\mathcal{B}$ such that $in_A: 0_\mathcal{A} \to A $ and $in_B: 0_\mathcal{B} \to B$. Thus we have a candidate morphism $(in_A, in_B)$. In order to check that this morphism is a morphism of $(F \downarrow G)$ we need to show that the following diagram is commutative: % https://q.uiver.app/#q=WzAsNCxbMCwwLCIwX1xcbWF0aGNhbHtDfSJdLFsyLDAsIkcwX1xcbWF0aGNhbHtCfSJdLFswLDIsIkZBIl0sWzIsMiwiR0IiXSxbMCwxLCJpbiIsMl0sWzAsMiwiRmluX0EiXSxbMiwzLCJmIl0sWzEsMywiR2luX0IiLDJdXQ== \[\begin{tikzcd} {F(0_\mathcal{A})=0_\mathcal{C}} && {G0_\mathcal{B}} \\ \\ FA && GB \arrow["in"', from=1-1, to=1-3] \arrow["{Fin_A}", from=1-1, to=3-1] \arrow["{Gin_B}"', from=1-3, to=3-3] \arrow["f", from=3-1, to=3-3] \end{tikzcd}\] The diagram above is trivially commutative: since $0_\mathcal{C}$ is intial in $\mathcal{C}$ both $f\circ Fin_A: 0_\mathcal{C} \to GB$ and $Gin_B \circ in: 0_\mathcal{C} \to GB$ must be equal to $in_{GB}: 0_\mathcal{C} \to GB$. Thus $$(0_\mathcal{A}, 0_\mathcal{B}, in) \xrightarrow{(in_A, in_B)} (A,B,f)$$ is a morphism in $(F \downarrow G)$ \item uniqueness: let $(0_\mathcal{A}, 0_\mathcal{B}, in) \xrightarrow[(h,k)]{(in_A, in_B)} (A,B,f)$ two arrows in $(F \downarrow G)$; then since $0_\mathcal{A}, 0_\mathcal{B}$ are initial, then $h = in_A$ and $k = in_B$; hence $(h,k)= (in_A,in_B)$ and so $(in_A,in_B)$ is unique \end{itemize} Thus $(F \downarrow G)$ admits initial object \\ \textbf{Pushouts}: As for the case above let construct the pushouts in $(F \downarrow G)$ by using pushout provided by cocompleteness of $\mathcal{A}, \mathcal{B}$. Take the following scenario in $(F \downarrow G)$ \begin{equation}\label{push_1} % https://q.uiver.app/#q=WzAsMyxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMCwxLCIoaCxrKSIsMl0sWzAsMiwiKGgnLGsnKSJdXQ== \begin{tikzcd} {(A,B,f)} && {(A',B',f')} \\ \\ {(A'',B'',f'')} \arrow["{(h,k)}"', from=1-1, to=1-3] \arrow["{(h',k')}", from=1-1, to=3-1] \end{tikzcd} \end{equation} then we can form two pushouts in $\mathcal{A} $ and $ \mathcal{B}$: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJBIl0sWzIsMCwiQSciXSxbMCwyLCJBJyciXSxbMiwyLCJQX0EiXSxbMywwLCJCIl0sWzMsMiwiQScnIl0sWzUsMCwiQiciXSxbNSwyLCJQX0IiXSxbMCwxLCJoIiwyXSxbMCwyLCJoJyJdLFsyLDMsInBfMiJdLFsxLDMsInBfMSIsMl0sWzMsMCwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzQsNSwiayciXSxbNCw2LCJrIiwyXSxbNiw3LCJxXzEiLDJdLFs1LDcsInFfMiJdLFs3LDQsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ== \[\begin{tikzcd} A && {A'} & B && {B'} \\ \\ {A''} && {P_A} & {A''} && {P_B} \arrow["h"', from=1-1, to=1-3] \arrow["{h'}", from=1-1, to=3-1] \arrow["{p_1}"', from=1-3, to=3-3] \arrow["k"', from=1-4, to=1-6] \arrow["{k'}", from=1-4, to=3-4] \arrow["{q_1}"', from=1-6, to=3-6] \arrow["{p_2}", from=3-1, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-3, to=1-1] \arrow["{q_2}", from=3-4, to=3-6] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-6, to=1-4] \end{tikzcd}\] Now, follwoing the same idea of initial object we may expect the pushout in $(F \downarrow G)$ to be $(P_A, P_B, u)$ for some $u: F(P_A) \to G(P_B)$. Now, we need to construct a candidate for $u$. Firs of all, since $F$ preserves finite colimits, $F(P_A)=P_A'$ is the pushout of $Fh: FA \to FA'$ and $Fh': FA \to FA''$ in $\mathcal{C}$ (wiht projection $\pi_1: FA' \to P_A', \pi_2: FA'' \to P_A'$ equal to $Fp_1$ and $Fp_2$ up to isomorphism). Then we have the following diagram: \begin{equation}\label{def-u} % https://q.uiver.app/#q=WzAsNSxbMCwwLCJGQSJdLFswLDIsIkZBJyciXSxbMiwwLCJGQSciXSxbMiwyLCJHUF9CIl0sWzEsMSwiUEEnIl0sWzAsMSwiRmgnIiwyXSxbMCwyLCJGaCJdLFsxLDRdLFsyLDRdLFs0LDMsIlxcZXhpc3RzICEgdSIsMl0sWzEsMywiRnFfMiBcXGNpcmMgZicnIiwyXSxbMiwzLCJGcV8xIFxcY2lyYyBmJyJdXQ== \begin{tikzcd} FA && {FA'} \\ & {P_A'} \\ {FA''} && {GP_B} \arrow["Fh", from=1-1, to=1-3] \arrow["{Fh'}"', from=1-1, to=3-1] \arrow[from=1-3, to=2-2] \arrow["{Fq_1 \circ f'}", from=1-3, to=3-3] \arrow["{\exists ! u}"', from=2-2, to=3-3] \arrow[from=3-1, to=2-2] \arrow["{Fq_2 \circ f''}"', from=3-1, to=3-3] \end{tikzcd} \end{equation} The external square is commutative since $Fq_1 \circ f' \circ Fh = Fq_1 \circ Fk \circ f = Fq_2 \circ Fk' \circ f = Fq_2 \circ f'' \circ Fh'$ (we used arrow condition of $(F \downarrow G)$ plus the fact that image under functor of commutative diagrams are indeed commutative). Thus there exists a unique $u: P_A' \to GP_B$ such $u \circ Fp_2 = Fq_2 \circ f''$ and $u \circ Fp_1 = Fp_1 \circ f'$. Now, we claim $(P_A,P_B,u)$ to be the pushout of (\ref{push_1}) with projections $(p_1,q_1): (A',B',f') \to (P_A,P_B,u)$ and $(p_2,q_2): (A'',B'',f'') \to (P_A, P_B, u)$. % https://q.uiver.app/#q=WzAsNCxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMiwyLCIoUF9BLCBQX0IsIHUpIl0sWzAsMSwiKGgsaykiXSxbMCwyLCIoaCcsaycpIiwyXSxbMSwzLCIocF8xLHFfMSkiXSxbMiwzLCIocF8yLHFfMikiLDJdXQ== \[\begin{tikzcd} {(A,B,f)} && {(A',B',f')} \\ \\ {(A'',B'',f'')} && {(P_A, P_B, u)} \arrow["{(h,k)}", from=1-1, to=1-3] \arrow["{(h',k')}"', from=1-1, to=3-1] \arrow["{(p_1,q_1)}", from=1-3, to=3-3] \arrow["{(p_2,q_2)}"', from=3-1, to=3-3] \end{tikzcd}\] Now, we shall prove that the projections are actually arrows of $(F \downarrow G)$ and that the universal property holds. \\ We begin proving that the projections are actually arrow, i.e. that the following diagrams are commutative: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJGQSciXSxbMiwwLCJHQiciXSxbMCwyLCJQJ19BIl0sWzIsMiwiR1BfQiJdLFszLDAsIkZBJyciXSxbMywyLCJQX0EnIl0sWzUsMCwiR0InJyJdLFs1LDIsIkdQX0IiXSxbMCwxLCJmJyJdLFswLDIsIkZwXzEiLDJdLFsxLDMsIkZxXzEiXSxbMiwzLCJ1IiwyXSxbNCw1LCJGcF8yIiwyXSxbNCw2LCJmJyciXSxbNSw3LCJ1IiwyXSxbNiw3LCJGcV8yIl1d \[\begin{tikzcd} {FA'} && {GB'} & {FA''} && {GB''} \\ \\ {P'_A} && {GP_B} & {P_A'} && {GP_B} \arrow["{f'}", from=1-1, to=1-3] \arrow["{Fp_1}"', from=1-1, to=3-1] \arrow["{Gq_1}", from=1-3, to=3-3] \arrow["{f''}", from=1-4, to=1-6] \arrow["{Fp_2}"', from=1-4, to=3-4] \arrow["{Gq_2}", from=1-6, to=3-6] \arrow["u"', from=3-1, to=3-3] \arrow["u"', from=3-4, to=3-6] \end{tikzcd}\] Both diagrams are commutative as consequence of the diagram (\ref{def-u}); hence projections are indeed arrows in $(F \downarrow G)$. \\ Now we prove that the universal propery holds: \begin{itemize} \item existence: assume the following diagram is commutative % https://q.uiver.app/#q=WzAsNCxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMiwyLCIoWCxZLGcpIl0sWzAsMSwiKGgsaykiXSxbMCwyLCIoaCcsaycpIiwyXSxbMSwzLCIoeCcseScpIl0sWzIsMywiKHgnJyx5JycpIiwyXV0= \[\begin{tikzcd} {(A,B,f)} && {(A',B',f')} \\ \\ {(A'',B'',f'')} && {(X,Y,g)} \arrow["{(h,k)}", from=1-1, to=1-3] \arrow["{(h',k')}"', from=1-1, to=3-1] \arrow["{(x',y')}", from=1-3, to=3-3] \arrow["{(x'',y'')}"', from=3-1, to=3-3] \end{tikzcd}\] First notice that since $(x',y')$ and $(x'',y'')$ are arrows of $(F \downarrow G)$ then \begin{align}\label{x'y'} g \cdot Fx' = Gy' \cdot f' \\ g \cdot Fx'' = Gy'' \cdot f''\label{x''y''} \end{align} Second, since the square is commutative, then we have the following two commutative diagram in $\mathcal{A}$ and $\mathcal{B}$ thanks to the universal property of $P_A$ and $P_B$: \begin{equation}\label{pushoutarrinAB} % https://q.uiver.app/#q=WzAsMTAsWzAsMCwiQSJdLFsyLDAsIkEnIl0sWzAsMiwiQScnIl0sWzEsMSwiUF9BIl0sWzMsMCwiQiJdLFszLDIsIkEnJyJdLFs1LDAsIkInIl0sWzQsMSwiUF9CIl0sWzIsMiwiWCJdLFs1LDIsIlkiXSxbMCwxLCJoIl0sWzAsMiwiaCciLDJdLFsyLDMsInBfMiJdLFsxLDMsInBfMSIsMl0sWzQsNSwiayciLDJdLFs0LDYsImsiXSxbNiw3LCJxXzEiLDJdLFs1LDcsInFfMiJdLFsyLDgsIngnJyIsMl0sWzEsOCwieCciXSxbNyw5LCJcXGV4aXN0IXVfQiJdLFs2LDksInknIl0sWzUsOSwieScnIiwyXSxbMyw4LCJcXGV4aXN0ISB1X0EiLDFdXQ== \begin{tikzcd} A && {A'} & B && {B'} \\ & {P_A} &&& {P_B} \\ {A''} && X & {A''} && Y \arrow["h", from=1-1, to=1-3] \arrow["{h'}"', from=1-1, to=3-1] \arrow["{p_1}"', from=1-3, to=2-2] \arrow["{x'}", from=1-3, to=3-3] \arrow["k", from=1-4, to=1-6] \arrow["{k'}"', from=1-4, to=3-4] \arrow["{q_1}"', from=1-6, to=2-5] \arrow["{y'}", from=1-6, to=3-6] \arrow["{\exists ! u_A}"{description}, from=2-2, to=3-3] \arrow["{\exists !u_B}"{description}, from=2-5, to=3-6] \arrow["{p_2}", from=3-1, to=2-2] \arrow["{x''}"', from=3-1, to=3-3] \arrow["{q_2}", from=3-4, to=2-5] \arrow["{y''}"', from=3-4, to=3-6] \end{tikzcd} \end{equation} Now, we claim that the following diagram is commutative: \begin{equation}\label{goalpush} % https://q.uiver.app/#q=WzAsNSxbMCwwLCIoQSxCLGYpIl0sWzAsMiwiKEEnJyxCJycsZicnKSJdLFsxLDEsIihQX0EsUF9CLHUpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFsyLDIsIihYLFksZykiXSxbMCwxXSxbMCwzXSxbMywyLCIocF8xLHFfMSkiLDJdLFsxLDQsIih4JycseScnKSIsMl0sWzMsNCwiKHgnLHknKSJdLFsyLDQsIih1X2EsdV9iKSIsMV0sWzEsMiwiKHBfMixxXzIpIl1d \begin{tikzcd} {(A,B,f)} && {(A',B',f')} \\ & {(P_A,P_B,u)} \\ {(A'',B'',f'')} && {(X,Y,g)} \arrow[from=1-1, to=1-3] \arrow[from=1-1, to=3-1] \arrow["{(p_1,q_1)}"', from=1-3, to=2-2] \arrow["{(x',y')}", from=1-3, to=3-3] \arrow["{(u_a,u_b)}"{description}, from=2-2, to=3-3] \arrow["{(p_2,q_2)}", from=3-1, to=2-2] \arrow["{(x'',y'')}"', from=3-1, to=3-3] \end{tikzcd} \end{equation} If $(u _A,u_B)$ is an arrow of $(F \downarrow G)$ then we are done, since the square is commutative as a direct consequence of the commutativity of (\ref{pushoutarrinAB}). Then we claim $(u_A,u_B)$ to be an actual arrow of $(F \downarrow G)$, i.e. we claim that the following diagram is commutative: \begin{equation}\label{uAuBarrow} % https://q.uiver.app/#q=WzAsNCxbMCwwLCJQJ19BIl0sWzIsMCwiR1BfQiJdLFswLDIsIkZYIl0sWzIsMiwiR1kiXSxbMCwxLCJ1Il0sWzAsMiwiRnVfQSIsMl0sWzIsMywiZyIsMl0sWzEsMywiR3VfQiJdXQ== \begin{tikzcd} {P'_A} && {GP_B} \\ \\ FX && GY \arrow["u", from=1-1, to=1-3] \arrow["{Fu_A}"', from=1-1, to=3-1] \arrow["{Gu_B}", from=1-3, to=3-3] \arrow["g"', from=3-1, to=3-3] \end{tikzcd} \end{equation} We will prove commutativity using that $P_A'$ is a pushout in $\mathcal{C}$. Indeed, consider the following diagram: % https://q.uiver.app/#q=WzAsNyxbMSwyLCJQJ19BIl0sWzMsMiwiR1BfQiJdLFsxLDQsIkZYIl0sWzMsNCwiR1kiXSxbMiwwLCJGQSJdLFswLDEsIkZBJyJdLFs0LDEsIkZBJyciXSxbMCwxLCJ1Il0sWzAsMiwiRnVfQSIsMl0sWzIsMywiZyIsMl0sWzEsMywiR3VfQiJdLFs0LDUsIkZoJyIsMl0sWzQsNiwiRmgnJyJdLFs1LDIsIkZ4JyIsMix7ImN1cnZlIjoyfV0sWzYsMywiZ0Z4JyciLDAseyJjdXJ2ZSI6LTJ9XSxbMCwzLCJcXGV4aXN0cyAhIHYiLDFdLFs1LDAsIkZwXzIiLDAseyJjdXJ2ZSI6LTF9XSxbNiwwLCJGcF8yIiwyLHsiY3VydmUiOjF9XV0= \[\begin{tikzcd} && FA && \\ {FA'} &&&& {FA''} \\ & {P'_A} && {GP_B} \\ \\ & FX && GY \arrow["{Fh'}"', from=1-3, to=2-1] \arrow["{Fh''}", from=1-3, to=2-5] \arrow["{Fp_1}", curve={height=-6pt}, from=2-1, to=3-2] \arrow["{Fx'}"', curve={height=12pt}, from=2-1, to=5-2] \arrow["{Fp_2}"', curve={height=6pt}, from=2-5, to=3-2] \arrow["{gFx''}", curve={height=-12pt}, from=2-5, to=5-4] \arrow["u", from=3-2, to=3-4] \arrow["{Fu_A}"', from=3-2, to=5-2] \arrow["{\exists ! v}"{description}, from=3-2, to=5-4] \arrow["{Gu_B}", from=3-4, to=5-4] \arrow["g"', from=5-2, to=5-4] \end{tikzcd}\] Then using (\ref{x'y'}) and (\ref{x''y''}) we can show that the external square is commuative: \begin{align*} g Fx'' Fh'' = Gy'' f'' Fh' = Gy'' Gk' f = Gy'Gkf \\ g Fx' Fh = Gy' f' Fh = Gy'Gkf \end{align*} Thus, by $P'_A$ beeing pushout in $\mathcal{C}$ there exists an unique $v: P_A' \to GY$ such that $vFp_1 = gFx'$ and $vFp_2 = gFx''$. Now , consider $gFu_A, Gu_Bu: P_A' \to GY$, notice that: \begin{align*} gFu_AFp_1 = gFx' \\ gFu_BFp_2 = gFx'' \\ Gu_BuFp_1 = Gu_BGq_1f' = Gy'f' = gFx' \\ Gu_BuFp_2 = Gu_BGq_2f'' = Gy''f'' = gFx'' \\ \end{align*} So by uniqueness of $v$ we get $gFu_A = Gu_B u$ and so, since the square (\ref{uAuBarrow}) is commutative, then $(u_A,u_B)$ is an arrow of $(F \downarrow G)$ and the diagram (\ref{goalpush}) is commutative. \item uniqueness: the uniquness of $(u_A,u_B)$ comes almost for free: indee if there was antoher arrow $(l,m)$ satisfyng commutativity in (\ref{goalpush}), then, by universal property of pushouts $l=u_A$ in $\mathcal{A}$ and $m = u_B$ in $\mathcal{B}$. Therefore we would have $(l,m) = (u_A, u_B)$ \end{itemize} Thus $(P_A, P_B, u)$ is the desired pushout and $(F \downarrow G)$ having initial object and pushouts is indeed finitely cocomplete. \\ \textbf{The forgetfoul functors are cocontinous}: the cocontinuity of $\Pi_1, \Pi_2$ arises immediatly from the structure of intial object and pushouts of $(F \downarrow G)$. Indeed take the inital object of $(F \downarrow G)$, $(0_A, 0_B, in)$; then $\Pi_1((0_A, 0_B, in))=0_A$ and $\Pi_2((0\_A, 0\_B, in)) = 0_B$ are respectively the initial object of $\mathcal{A}$ and $\mathcal{B}$. Since the same happens for the pushouts of $(F \downarrow G)$ then both $\Pi_1$ and $\Pi_2$ preserves finite colimits. \\ Now, let's move on to the finitely complete case; so suppose that both $\mathcal{A}$ and $\mathcal{B}$ are finitely complete and that $G$ is finitely continous. The structure of the proof is completely analogue \footnote{Notice that we can also argue that, beeing $(F \downarrow G)^{op} \cong (F^{op} \downarrow G^{op})$, the complete case comes for free from the cocomplete case} and so we will omit some details. \\ \textbf{Terminal Objects}: following the structure of the cocomplete proof we claim $(1_\mathcal{A}, 1_\mathcal{B}, un)$, where $un: F(1_\mathcal{A}) \to 1_\mathcal{C} = G(1_\mathcal{B})$ is the unique morphism granted by $G(1_\mathcal{B})$ be terminal in $\mathcal{C}$, to be the terminal object in $(F \downarrow G)$ \begin{itemize} \item existence: let $(A,B,f)$ be an object of $(F\downarrow G)$; then there exists two unique morphisms $un_A, un_B$ respectively in $\mathcal{A}$ and $\mathcal{B}$ such that $un_A: A \to 1_\mathcal{A} $ and $un_B: B \to 1_\mathcal{B}$. Thus we have a candidate morphism $(un_A, un_B)$. In order to check that this morphism is a morphism of $(F \downarrow G)$ we need to show that the following diagram is commutative: \[\begin{tikzcd} {F1_\mathcal{A}} && {G1_\mathcal{B}= 1_\mathcal{C}} \\ \\ FA && GB \arrow["un"', from=1-1, to=1-3] \arrow["{Fun_A}", from=1-1, to=3-1] \arrow["{Gun_B}"', from=1-3, to=3-3] \arrow["f", from=3-1, to=3-3] \end{tikzcd}\] The diagram above is trivially commutative since $G1_\mathcal{B} = 1_\mathcal{C}$ is terminal in $\mathcal{C}$ \item uniqueness: the uniquness is directly inherited by uniness of $un_A$ and $un_B$ in $\mathcal{A}$ and $\mathcal{B}$ \end{itemize} \textbf{Pullbacks}: As for the pushouts we claim the pullback of the following diagram: % https://q.uiver.app/#q=WzAsMyxbMCwyLCIoQScsQicsZikiXSxbMiwyLCIoQScnLEInJyxmJycpIl0sWzIsMCwiKEEsQixmKSJdLFswLDEsIihoJyxrJykiXSxbMiwxLCIoaCxrKSIsMl1d \[\begin{tikzcd} && {(A,B,f)} \\ \\ {(A',B',f)} && {(A'',B'',f'')} \arrow["{(h,k)}"', from=1-3, to=3-3] \arrow["{(h',k')}", from=3-1, to=3-3] \end{tikzcd}\] to be $(P_A , P_B, u)$ with projections $(p_1,q_1): (P_A,P_B,u) \to (A,B,f)$ and $(p_2,q_2): (P_A,P_B,u) \to (A',B',f')$ where $(P_A, p_1, p_2)$ and $(P_B, q_1, q_2)$ are pullbacks in $\mathcal{A}$ and $\mathcal{B}$ (Remember that $GP_B=P_B'$ is a pullback in $\mathcal{C}$ as was for $FP_A$ in the cocomplete case). $u: FP_A \to P_B'$ arises from the universal property of $P_B'$ as shown in the following diagram (whose commutativity is ensured by arrow condition in $(F \downarrow G)$ plus pullbacks condition of $(P_A, q_1, q_2)$ in $\mathcal{A}$): % https://q.uiver.app/#q=WzAsNixbMSwzLCJHQiciXSxbMywzLCJHQicnIl0sWzMsMSwiR0IiXSxbMSwxLCJQJ19CIl0sWzAsMCwiUF9BIl0sWzEsNV0sWzAsMSwiR2snIl0sWzIsMSwiR2siLDJdLFszLDAsIkdxXzIiXSxbMywyLCJHcV8xIiwyXSxbNCwwLCJmJ0ZwXzIiLDIseyJjdXJ2ZSI6Mn1dLFs0LDIsImZGcF8xIiwyLHsiY3VydmUiOi0yfV0sWzQsMywiXFxleGlzdHMgISB1IiwxXV0= \[\begin{tikzcd} {P_A} &&& \\ & {P'_B} && GB \\ \\ & {GB'} && {GB''} \\ \\ & {} \arrow["{\exists ! u}"{description}, from=1-1, to=2-2] \arrow["{fFp_1}"', curve={height=-12pt}, from=1-1, to=2-4] \arrow["{f'Fp_2}"', curve={height=12pt}, from=1-1, to=4-2] \arrow["{Gq_1}"', from=2-2, to=2-4] \arrow["{Gq_2}", from=2-2, to=4-2] \arrow["Gk"', from=2-4, to=4-4] \arrow["{Gk'}", from=4-2, to=4-4] \end{tikzcd}\] From the commutativity of this diagram we deduce that $(q_i, p_i)$ are actuall arrows of $(F \downarrow G)$, indeed: \begin{align} Gq_2u = f'Fp_2 \\ Gq_1u = fFp_1 \end{align} Now, we cheeck that the universal propery holds \begin{itemize} \item Existence: assume the external square to be commutative: \begin{equation}\label{pull} % https://q.uiver.app/#q=WzAsNixbMSwzLCIoQScsQicsZicpIl0sWzMsMywiKEEnJyxCJycsZicnKSJdLFszLDEsIihBLEIsZikiXSxbMCwwLCIoWCxZLGcpIl0sWzEsNV0sWzEsMSwiKFBfQSxQX0IsdSkiXSxbMCwxLCIoaCcsaycpIl0sWzIsMSwiKGgsaykiLDJdLFszLDAsIih4Jyx5JykiLDIseyJjdXJ2ZSI6Mn1dLFszLDIsIih4JycseScnKSIsMCx7ImN1cnZlIjotMn1dLFs1LDIsIihwXzEscV8xKSJdLFs1LDAsIihwXzIscV8yKSJdXQ== \begin{tikzcd} {(X,Y,g)} &&& \\ & {(P_A,P_B,u)} && {(A,B,f)} \\ \\ & {(A',B',f')} && {(A'',B'',f'')} \\ \\ & {} \arrow["{(x,y)}", curve={height=-12pt}, from=1-1, to=2-4] \arrow["{(x',y')}"', curve={height=12pt}, from=1-1, to=4-2] \arrow["{(p_1,q_1)}", from=2-2, to=2-4] \arrow["{(p_2,q_2)}", from=2-2, to=4-2] \arrow["{(h,k)}"', from=2-4, to=4-4] \arrow["{(h',k')}", from=4-2, to=4-4] \end{tikzcd} \end{equation} Then we can use universal property of $P_A$ and $P_B$ in $\mathcal{A}$ and $\mathcal{B}$: \begin{equation}\label{pullstart} % https://q.uiver.app/#q=WzAsMTAsWzAsMCwiWCJdLFsxLDEsIlBfQSJdLFszLDEsIkEiXSxbMSwzLCJBJyJdLFszLDMsIkEnJyJdLFs1LDEsIlBfQiJdLFs3LDEsIkIiXSxbNSwzLCJCJyJdLFs3LDMsIkInJyJdLFs0LDAsIlkiXSxbMSwyXSxbMSwzXSxbMyw0LCJoJyIsMl0sWzIsNCwiaCJdLFswLDMsIngnIiwwLHsiY3VydmUiOjJ9XSxbMCwyLCJ4IiwwLHsiY3VydmUiOi0yfV0sWzUsNl0sWzUsN10sWzcsOCwiayciLDJdLFs2LDgsImsiXSxbOSw3LCJ5JyIsMCx7ImN1cnZlIjoyfV0sWzksNiwieSIsMCx7ImN1cnZlIjotMn1dLFswLDEsIlxcZXhpc3RzICEgdV9BIiwxXSxbOSw1LCJcXGV4aXN0cyAhIHVfQiIsMV1d \begin{tikzcd} X &&&& Y &&& \\ & {P_A} && A && {P_B} && B \\ \\ & {A'} && {A''} && {B'} && {B''} \arrow["{\exists ! u_A}"{description}, from=1-1, to=2-2] \arrow["x", curve={height=-12pt}, from=1-1, to=2-4] \arrow["{x'}", curve={height=12pt}, from=1-1, to=4-2] \arrow["{\exists ! u_B}"{description}, from=1-5, to=2-6] \arrow["y", curve={height=-12pt}, from=1-5, to=2-8] \arrow["{y'}", curve={height=12pt}, from=1-5, to=4-6] \arrow[from=2-2, to=2-4] \arrow[from=2-2, to=4-2] \arrow["h", from=2-4, to=4-4] \arrow[from=2-6, to=2-8] \arrow[from=2-6, to=4-6] \arrow["k", from=2-8, to=4-8] \arrow["{h'}"', from=4-2, to=4-4] \arrow["{k'}"', from=4-6, to=4-8] \end{tikzcd} \end{equation} Now, consider the couple $(u_A,u_B)$; by commutativity of (\ref{pullstart}) if $(u_A,u_B): (X,Y,g) \to (P_A,P_B, u)$ is an actual arrow of $(F \downarrow G)$ then it complete the diagram (\ref{pull}) to a commutative diagram. \\ We procede as in the case of pushouts; consider the following square: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJGWCJdLFsxLDAsIkdZIl0sWzEsMSwiR3VfQiBcXGNvbmcgUF9CJyJdLFswLDEsIkZQX0EiXSxbMSwyLCJHQiciXSxbMiwyLCJHQicnIl0sWzIsMSwiR0IiXSxbMCwyLCJGQSciXSxbMCwxLCJnIl0sWzEsMl0sWzAsM10sWzMsMiwidSIsMl0sWzIsNCwiR3FfMiJdLFs0LDUsIkdrJyIsMl0sWzIsNiwiR3FfMSIsMl0sWzYsNSwiR2siXSxbMCwyLCJcXGV4aXN0cyAhIHYgIiwxXSxbMSw2LCJHeSIsMCx7ImN1cnZlIjotMn1dLFs3LDQsImYnIiwyXSxbMCw3LCJGeCciLDIseyJjdXJ2ZSI6NH1dXQ== \[\begin{tikzcd} FX & GY & \\ {FP_A} & {Gu_B \cong P_B'} & GB \\ {FA'} & {GB'} & {GB''} \arrow["g", from=1-1, to=1-2] \arrow[from=1-1, to=2-1] \arrow["{\exists ! v }"{description}, from=1-1, to=2-2] \arrow["{Fx'}"', curve={height=24pt}, from=1-1, to=3-1] \arrow[from=1-2, to=2-2] \arrow["Gy", curve={height=-12pt}, from=1-2, to=2-3] \arrow["u"', from=2-1, to=2-2] \arrow["{Gq_1}"', from=2-2, to=2-3] \arrow["{Gq_2}", from=2-2, to=3-2] \arrow["Gk", from=2-3, to=3-3] \arrow["{f'}"', from=3-1, to=3-2] \arrow["{Gk'}"', from=3-2, to=3-3] \end{tikzcd}\] Since $(x',y')$ and $(x,y)$ are arrows of $(F \downarrow G)$, the square (\ref{pull}) is commutative and using the definition of $(p_i,q_i)$ we can show that the external square commutes, indeed: \begin{equation} Gk'f'Fx'=Gk'Gy'g=GkGyg \end{equation} Thus, since $P_B'$ is the pullback of $GB \xrightarrow{Gk} GB''$ and $GB' \xrightarrow{Gk'} GB''$ there exists an unique $v : FX \to P_B'$ such $Gq_1v = Gy g$ and $Gq_2v = f' Fx'$. Now, consider $uFu_A,Gu_Bg : FX \to P_B'$ and notice that: \begin{align*} Gq_1uFu_A = f Fp_1 Fu_A = f Fx = Gyg \\ Gq_2uFu_A = f Fp_2Fu_A = f' Fp_2 F u_A = f'Fx' \\ Gq_1Gu_Bg = Gy g \\ Gq_2Gu_Bg = Gy'g = f'Fx' \\ \end{align*} Thus by uniqueness of $v: FX \to P_B'$ then $uFu_A = Gu_B f$ and so $(u_A,u_B): (X,Y,g) \to (P_A,P_B,u)$ is an arrow of $(F \downarrow G)$ and complete the diagram (\ref{pull}) to a commutative diagram \item uniqueness: uniqueness of $u_A$ and $u_B$ in $\mathcal{A}$ and $\mathcal{B}$ yields to uniqueness of $(u_A,u_B)$ in $(F \downarrow G)$ \end{itemize} \textbf{Forgetful functors are continous}: the proof is analogue to the cocomplete case, since both $\Pi_1,\Pi_2$ preserves terminal object and pullbacks. \\ We proved that under the assumption of $\mathcal{A}$ and $\mathcal{B}$ beeing cocomplete and $F$ beeing cocontinous the comma category $(F \downarrow G)$ is cocomplete and that $\Pi_i$ is cocontinous; morevoer we proved the dual result with complteness assumption, therefore the statement is proved and we are done. \end{proof} \begin{definition}[Freyd Cover] Let $\mathcal{C}$ be a small category (serve veramente sia piccola?) with a terminal odject $1$, then we call its \textit{Freyd Cover}, $Cov(\mathcal{C})$, the comma category $Id \downarrow \mathcal{C}(1,\text{-})$ where $Id: Set \to Set$ is the identical functor \end{definition} \begin{definition}[Projection Functor of Freyd Cover] Recall that there are two canonical functors $\Pi_1,\Pi_2$ associated with a comma category. Let $\mathcal{C}$ be a category with terminal object and let $Cov(\mathcal{C})$ be its Frey Cover. We call the functor $\Pi_2: Cov(\mathcal{C}) \to \mathcal{C}$ the projection functor of the Freyd Cover. \end{definition} \begin{theorem}\label{cover of bicartesian} Let $\mathcal{C}$ be a bicartesian category - i.e. a category with terminal object, initial object and binary products and coproducs - then $Cov(\mathcal{C})$ is bicartesian. Moreover $\Pi_2 : Cov(\mathcal{C}) \to \mathcal{C}$ is a cartesian closed functor \end{theorem} \begin{proof} The proof follows a similar structure to the proof of \ref{completenesscomma}, so we will construct initial and terminal objects, binary products and copruducts and then we will prove that $\Pi_2$ is closed with respect to this constructions. \\ \textbf{Initial and Terminal Object}: the initial object of $Cov(\mathcal{C})$ is $(0_{Set}, 0_\mathcal{C}, in)$ and the terminal object is $(1_{Set}, 1_\mathcal{C}, un)$. The construction is the same of the construction in \ref{completenesscomma} and therefore the proof is ommitted \\ \textbf{Binary Products}: Recall that $\mathcal{C}(1_\mathcal{C},-): \mathcal{C} \to Set$ is a continous functor - i.e. preserves limits - and so in particular it preserves binary products. Therefore if $A,B$ are objects of $\mathcal{C}$ we have a set isomorphism $\sigma$: % https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQSBcXHRpbWVzIEIpIl0sWzAsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBKSBcXHRpbWVzIFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsIihoLCBrKSJdLFsxLDEsIjwgaCxrID46IDFfXFxtYXRoY2Fse0N9IFxcdG8gQSBcXHRpbWVzIEIgIl0sWzEsMF0sWzIsMywiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dXQ== \[\begin{tikzcd} {\mathcal{C}(1_\mathcal{C}, A) \times \mathcal{C}(1_\mathcal{C},B)} & {\mathcal{C}(1_\mathcal{C},A \times B)} \\ {(h, k)} & {< h,k >: 1_\mathcal{C} \to A \times B } \arrow[from=1-1, to=1-2] \arrow[maps to, from=2-1, to=2-2] \end{tikzcd}\] Now, let $(X,A,f),(Y,B,g)$ be two object of $Cov(\mathcal{C})$; we claim their product to be $(X\times Y, A \times B, \sigma \circ (f \times g))$ where $\sigma \circ (f \times f)$ arises from the following produt diagram in $Set$: % https://q.uiver.app/#q=WzAsNyxbMCwxLCJYIFxcdGltZXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpXFx0aW1lcyBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQSkiXSxbNCwxLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQVxcdGltZXMgQikiXSxbMCwxLCJcXHBpX1giXSxbMCwyLCJcXHBpX1kiLDJdLFsxLDMsImYiXSxbMiw0LCJnIiwyXSxbNSwzLCJcXHBpXzEiLDJdLFs1LDQsIlxccGlfMiJdLFswLDUsIlxcZXhpc3RzICEgPGZcXHBpX3gsZ1xccGlfeT4gOj0gZiBcXHRpbWVzIGciXSxbNSw2LCJcXHNpZ21hIl1d \[\begin{tikzcd} & X & {\mathcal{C}(1_\mathcal{C},A)} && \\ {X \times Y} &&& {\mathcal{C}(1_\mathcal{C},A)\times \mathcal{C}(1_\mathcal{C},A)} & {\mathcal{C}(1_\mathcal{C},A\times B)} \\ & Y & {\mathcal{C}(1_\mathcal{C},B)} \arrow["f", from=1-2, to=1-3] \arrow["{\pi_X}", from=2-1, to=1-2] \arrow["{\exists ! := f \times g}", from=2-1, to=2-4] \arrow["{\pi_Y}"', from=2-1, to=3-2] \arrow["{\pi_1}"', from=2-4, to=1-3] \arrow["\sigma", from=2-4, to=2-5] \arrow["{\pi_2}", from=2-4, to=3-3] \arrow["g"', from=3-2, to=3-3] \end{tikzcd}\] and we claim the projections of $(X\times Y, A \times B, \sigma \circ (f \times g))$ to be $(\pi_X,\pi_A):(X\times Y, A \times B, \sigma \circ (f \times g)) \to (X, A,f)$ and $(\pi_Y,\pi_B):(X\times Y, A \times B, \sigma \circ (f \times g)) \to (Y, B,f)$. \\ We start by checking that our candidate projections are arrows of $Cov(\mathcal{C})$ and then we will check that the universal property holds. In order to check that our projection are actual arrows we shall prove that $ \mathcal{C}(1_\mathcal{C},\pi_A) \sigma (f \times g) = f \pi_X$ and that $\mathcal{C}(1_\mathcal{C}, \pi_B) \sigma (f \times g) = \pi_B g$ but this two identities follow directly from the fact that $\mathcal{C}(1_\mathcal{C},-)$ preserves products and that products are unique up to ismorphism, thus $\pi_1 = \mathcal{C}(\_\mathcal{C},-)\pi_A$ and $\pi_2 = \mathcal{C}(\_\mathcal{C},-)\pi_B$ and so the indentity are trivial. Let's move on to the universal property. \begin{itemize} \item existence: let consider the following situation: \begin{equation}\label{prodgoal} % https://q.uiver.app/#q=WzAsNCxbMSwwLCIoWFxcdGltZXMgWSwgQSBcXHRpbWVzIEIsIFxcc2lnbWEgKGYgXFx0aW1lcyBnKSkiXSxbMCwyLCIoWCxBLGYpIl0sWzIsMiwiKFksQixnKSAiXSxbMSwyLCIoWixDLGgpIl0sWzAsMSwiKFxccGlfWCwgXFxwaV9BKSIsMl0sWzAsMiwiKFxccGlfWSwgXFxwaV9CKSJdLFszLDIsIihsJyxtJykiLDJdLFszLDEsIihsLG0pIl1d \begin{tikzcd} & {(X\times Y, A \times B, \sigma (f \times g))} & \\ \\ {(X,A,f)} & {(Z,C,h)} & {(Y,B,g) } \arrow["{(\pi_X, \pi_A)}"', from=1-2, to=3-1] \arrow["{(\pi_Y, \pi_B)}", from=1-2, to=3-3] \arrow["{(l,m)}", from=3-2, to=3-1] \arrow["{(l',m')}"', from=3-2, to=3-3] \end{tikzcd} \end{equation} then, since $X \times Y$ and $A \times B$ are product rispectively in $Set$ and $\mathcal{C}$ we have the following commutative diagrams: % https://q.uiver.app/#q=WzAsOCxbMSwwLCJYXFx0aW1lcyBZIl0sWzAsMSwiWCJdLFsyLDEsIlkiXSxbMSwxLCJaIl0sWzMsMSwiQSJdLFs0LDAsIkEgXFx0aW1lcyBCIl0sWzUsMSwiQiJdLFs0LDEsIkMiXSxbMCwxLCJcXHBpX1giLDJdLFswLDIsIlxccGlfWSJdLFszLDEsImwiXSxbMywyLCJsJyIsMl0sWzMsMCwiXFxleGlzdHMgISBcXGJhcntsfSIsMV0sWzUsNCwiXFxwaV9BIiwyXSxbNSw2LCJcXHBpX0IiXSxbNyw0LCJtIl0sWzcsNiwibSciLDJdLFs3LDUsIlxcZXhpc3RzICEgXFxiYXJ7bX0iLDFdXQ== \[\begin{tikzcd} & {X\times Y} &&& {A \times B} & \\ X & Z & Y & A & C & B \arrow["{\pi_X}"', from=1-2, to=2-1] \arrow["{\pi_Y}", from=1-2, to=2-3] \arrow["{\pi_A}"', from=1-5, to=2-4] \arrow["{\pi_B}", from=1-5, to=2-6] \arrow["{\exists ! \bar{l}}"{description}, from=2-2, to=1-2] \arrow["l", from=2-2, to=2-1] \arrow["{l'}"', from=2-2, to=2-3] \arrow["{\exists ! \bar{m}}"{description}, from=2-5, to=1-5] \arrow["m", from=2-5, to=2-4] \arrow["{m'}"', from=2-5, to=2-6] \end{tikzcd}\] Thus consider the couple $(\bar{l},\bar{m})$; if it is a morphism of $Cov(\mathcal{C})$ then it completes the diagram (\ref{prodgoal}) to a commutative diagram. Now, consider the following diagram: % https://q.uiver.app/#q=WzAsOCxbMSwwLCJaIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEMpIl0sWzEsMSwiWCBcXHRpbWVzIFkiXSxbMiwxLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEEgXFx0aW1lcyBCKSJdLFswLDEsIlkiXSxbMiwyLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEEpXFx0aW1lcyBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEIpIl0sWzMsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBKSJdLFsxLDIsIlxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsImgiXSxbMCwyLCJcXGJhcntsfSJdLFsyLDNdLFsxLDMsIlxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSwgXFxiYXJ7bX0pIl0sWzAsNCwibCciLDJdLFsyLDUsImYgXFx0aW1lcyBnIiwxXSxbNSwzLCJcXHNpZ21hIiwwLHsiY3VydmUiOi0yfV0sWzMsNSwiXFxzaWdtYV4tMSIsMCx7Im9mZnNldCI6LTMsImN1cnZlIjotMX1dLFs1LDYsIlxccGlfMSIsMl0sWzUsNywiXFxwaV8yIl0sWzQsNywiZyIsMix7ImN1cnZlIjoyfV0sWzEsNiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LG0pIiwwLHsiY3VydmUiOi01fV0sWzUsMywiXFxjb25nIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d \[\begin{tikzcd} & Z & {\mathcal{C}(1_\mathcal{C},C)} & \\ Y & {X \times Y} & {\mathcal{C}(1_\mathcal{C}, A \times B)} \\ & {\mathcal{C}(1_\mathcal{C},B)} & {\mathcal{C}(1_\mathcal{C}, A)\times \mathcal{C}(1_\mathcal{C}, B)} & {\mathcal{C}(1_\mathcal{C}, A)} \arrow["h", from=1-2, to=1-3] \arrow["{l'}"', from=1-2, to=2-1] \arrow["{\bar{l}}", from=1-2, to=2-2] \arrow["{\mathcal{C}(1_\mathcal{C}, \bar{m})}", from=1-3, to=2-3] \arrow["{\mathcal{C}(1_\mathcal{C},m)}", curve={height=-30pt}, from=1-3, to=3-4] \arrow["g"', curve={height=12pt}, from=2-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow["{f \times g}"{description}, from=2-2, to=3-3] \arrow["{\sigma^-1}", shift left=3, curve={height=-6pt}, from=2-3, to=3-3] \arrow["\sigma", curve={height=-12pt}, from=3-3, to=2-3] \arrow["\cong"{description}, draw=none, from=3-3, to=2-3] \arrow["{\pi_2}", from=3-3, to=3-2] \arrow["{\pi_1}"', from=3-3, to=3-4] \end{tikzcd}\] Since $\pi_1\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = \mathcal{C}(1_\mathcal{C}, m)h = \pi_1 (f \times g)\bar{l}$ and $\pi_2\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = gl' = \pi_2 (f \times g)\bar{l} $ then by the universal property of binary product $\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = \sigma^{-1} \sigma (f \times g) \bar{l}$ hence $\sigma (f \times g) \bar{l} = \mathcal{C}(1_\mathcal{C},\bar{m})h$ thus $(\bar{l}, \bar{m})$ is an arrow of $Cov(\mathcal{C})$ and complete the diagram (\ref{prodgoal}) to a commutative diagram \item Uniqueness: uniqueness of $(\bar{l}, \bar{m})$ is directly inherited by uniqueness of $\bar{l}$ and $\bar{m}$ in $\mathcal{A}$ and $\mathcal{B}$ \end{itemize} \textbf{Binary Coproducts}: Let $(X,A ,f)$ and $(Y,B,g)$ be two objects of $Cov(\mathcal{C})$, then we claim their coprduct to be $(X \oplus Y, A \oplus B, f \oplus g)$ with injections $(\iota_X, \iota_A)$ and $(\iota_Y, \iota_B)$ where $f \oplus g$ arises from: % https://q.uiver.app/#q=WzAsNixbMCwxLCJYIFxcb3BsdXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpXFxvcGx1c1xcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSBcXGNvbmcgXFxtYXRoY2Fse0MoMV9cXG1hdGhjYWx7Q319LEEgXFxvcGx1cyBCKSJdLFsxLDAsIlxcaW90YV9YIiwyXSxbMiwwLCJcXGlvdGFfWSJdLFsxLDMsImYiXSxbMiw0LCJnIiwyXSxbNCw1LCJcXGlvdGFfMiIsMl0sWzMsNSwiXFxpb3RhXzEiXSxbMCw1LCJcXGV4aXN0cyAhIGYgXFxvcGx1cyBnIiwyXV0= \[\begin{tikzcd} & X & {\mathcal{C}(1_\mathcal{C},A)} & \\ {X \oplus Y} &&& {\mathcal{C}(1_\mathcal{C},A)\oplus\mathcal{C}(1_\mathcal{C},B) \cong \mathcal{C}(1_\mathcal{C},A \oplus B)} \\ & Y & {\mathcal{C}(1_\mathcal{C},B)} \arrow["f", from=1-2, to=1-3] \arrow["{\iota_X}"', from=1-2, to=2-1] \arrow["{\iota_1}", from=1-3, to=2-4] \arrow["{\exists ! f \oplus g}"', from=2-1, to=2-4] \arrow["{\iota_Y}", from=3-2, to=2-1] \arrow["g"', from=3-2, to=3-3] \arrow["{\iota_2}"', from=3-3, to=2-4] \end{tikzcd}\] The proof is analogue to the proof of binary product and so we omit the calculations. \\ \textbf{Projection is cartesian closed}: the proof of $\Pi_2$ beeing cartesian closed functor is identical to the proof of $\Pi_1$ beeing continous in \ref{completenesscomma} \end{proof} \begin{theorem} Let $\mathcal{H}$ be an Heyting Algebra - i.e. an ordered bicartesian category which is also cartesian closed - then $Cov(\mathcal{H})$ is also bicartesian closed. Morover the projection $\Pi_2 : Cov(\mathcal{H}) \to \mathcal{H}$ is bicartesian closed. \end{theorem} \begin{proof}\label{coverheyting} By \ref{cover of bicartesian} we know that $Cov(\mathcal{H})$ is bicartesian and that $\Pi_2$ is cartesian closed. So we need only to prove the existence of function spaces. \\ Let $(X,a,f)$ and $(Y,b,g)$ be objects of $Cov(\mathcal{C})$. We expect the exponential $(Y,b,g)^{(X,a,f)}$ to be something similar to $(Y^X, a \to b, \xi)$ where $Y^X = Set(X,Y)$ is the function space in $Set$, $a \to b$ is the heyting implication in $\mathcal{H}$ and $\xi$ is a function somehow defined using that beeing $\mathcal{H}$ an ordered category if $a \to b$ in nonempty the in terminal in $Set$. This intuition is almost correct, but there is a problem: in order to make $(Y^X, a \to b, \xi)$ an object of $\mathcal{H}$ we need $\xi: Y^X \to \mathcal{H}(1_\mathcal{H}, a \to b)$ to be a $Set$-morphism which is not possible if $ 1_\mathcal{H} \nleq_{\mathcal{H}} a \to b $ and $Y^X \neq \emptyset$. Thus we claim $(Y,b,g)^{(X,a,f)}$ to be $( (Y^X)_{a \leq b}, a \to b , \xi)$ where $(Y^X)_{a \leq b}$ is $Set(X,Y)$ if $a \leq_{\mathcal{H}} b$ - and so $\mathcal{H}(1_\mathcal{H}, a \to b) \neq \emptyset$ - and to be empty otherwise: \begin{equation*} (Y^X)_{a \leq b} := \{ h \in Y^X | \forall x \in X (f(x)\in \mathcal{H}(1_\mathcal{H},a) \implies g(h(x)) \in \mathcal{H}(1_\mathcal{H},b) )\} \end{equation*} with evaluation given by: $(Ev_{Set}, Ev_\mathcal{H}): ((Y^X)_{a \leq b}, a \to b, \xi) \to (Y, b, g)$ where $Ev_{Set} : (Y^X)_{a \leq b} \times X \to Y$ is the restriction of usual evaluation morphism in $Set$ and $Ev_\mathcal{H} = a \to b \land a \leq b$ is the counit of the adjunction of exponential functor in $\mathcal{H}$. Now, let $(u, c\land a \leq b) : (Z,c,h) \times (X,a,f) \to (Y,b,g)$, we claim its abstraction to be: \begin{equation*} (\hat{u}, c \leq a \to b) : (Z,c,h) \to ( (Y^X)_{a \leq b}, a \to b, \xi ) \end{equation*} This couple is clearly an arrow of $Cov(\mathcal{C})$\footnote{the arrow condition is forced since if every definition is coherent than the commutativity of the arrow condition square follows from $\mathcal{H}(1_\mathcal{H}, a \to b)$ be either termial or empty}. We claim that, if the abstraction is well defined, then the following diagram is commutative: \begin{equation}\label{exp goal} % https://q.uiver.app/#q=WzAsMyxbMCwyLCIoKFleWClfe2EgXFxsZXEgYn0sIGEgXFx0byBiLCBcXHhpKSAiXSxbMCwwLCIoWCwgYSxmKSBcXHRpbWVzIChaLGMsIGgpIl0sWzIsMiwiKFkpIl0sWzEsMiwiKHUsIGMgXFxsYW5kIGEgXFxsZXEgYikiXSxbMCwyLCIoRXZfe1NldH0sRXZfXFxtYXRoY2Fse0h9KSIsMl0sWzEsMCwiKFxcaGF0e3V9LCBjIFxcbGVxIGEgXFx0byBiICApIiwyXV0= \begin{tikzcd} {(X, a,f) \times (Z,c, h)} && \\ \\ {((Y^X)_{a \leq b}, a \to b, \xi) } && {(Y)} \arrow["{(\hat{u}, c \leq a \to b )}"', from=1-1, to=3-1] \arrow["{(u, c \land a \leq b)}", from=1-1, to=3-3] \arrow["{(Ev_{Set},Ev_\mathcal{H})}"', from=3-1, to=3-3] \end{tikzcd} \end{equation} Now, commutativity at the level of $Set$ is ensured by universal property of $Y^X$ in $Set$ plus the coerence condition of $(Y^X)_{a \leq b}$ with respect to $a \to b$. Now, in $\mathcal{H}$ we have that $c \land a \leq b$ we have that $c\land a \leq b \iff c \leq a \to b$ so we have commutativity at the level of $\mathcal{H}$. It remains to check the well definition of the abstraction: let $Z \neq \emptyset$, then $h(m) \in \mathcal{H}(1_\mathcal{H}, c)$ for $m \in Z$, hence $1_\mathcal{H} \leq c$ and so, since $c \land a \leq b$, then $a \leq b$ and so $\hat{u} (m) \in (Y^X)_{a \leq b}$ wihch ensure well definition of abstraction arrows. Notice that uniqueness of abstraction follows directly form uniqueness of abstractions in $Set$ and $\mathcal{H}$. Thus $Cov(\mathcal{H})$ is a bicartesian cloed category.\\ Concerning $\Pi_2$, the proof is identical to \ref{completenesscomma} since the $\mathcal{H}$ level of the exponential object is the exponential object in $\mathcal{H}$ and so $\Pi_2$ is a bicartesian closed functor and we are done. \end{proof} \begin{definition} Let $\mathcal{H}$ be an Heyting Algebra, then we call its Feryd cover the Frey-Heyting cover of $\mathcal{H}$ \end{definition} \begin{definition} We say that $\textbf{biCC}$ is the category with objects bicartesian closed categories and morphisms functors preserving the bicartesian structure up to isomorphism \end{definition} \begin{definition}[Global Set Functor] Let $\mathcal{C}$ be a locally small category with terminal object $1_\mathcal{C}$. We define the global set functor as: % https://q.uiver.app/#q=WzAsNixbMCwwLCJcXG1hdGhjYWx7Q30iXSxbMiwwLCJTZXQiXSxbMCwxLCJBIl0sWzAsMiwiQiJdLFsyLDEsIlxcR2FtbWEoQSk9IFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxBKSJdLFsyLDIsIlxcR2FtbWEoQik9IFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsIlxcR2FtbWEoLSkiXSxbMiwzXSxbNCw1LCJcXEdhbW1hKGYpPSBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sZikiXSxbMiw0LCJcXEdhbW1hKC0pIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs3LDgsIiIsMCx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d \[\begin{tikzcd} {\mathcal{C}} && Set \\ A && {\Gamma(A)= \mathcal{C}(1_\mathcal{C},A)} \\ B && {\Gamma(B)= \mathcal{C}(1_\mathcal{C},B)} \arrow["{\Gamma(-)}", from=1-1, to=1-3] \arrow["{\Gamma(-)}", maps to, from=2-1, to=2-3] \arrow[""{name=0, anchor=center, inner sep=0}, from=2-1, to=3-1] \arrow[""{name=1, anchor=center, inner sep=0}, "{\Gamma(f)= \mathcal{C}(1_\mathcal{C},f)}", from=2-3, to=3-3] \arrow[between={0.2}{0.8}, maps to, from=0, to=1] \end{tikzcd}\] \end{definition} \begin{lemma} Let $\mathcal{C}$ be a category in \textbf{biCC}, then its freyd cover $Cov(\mathcal{C})$ is again in \textbf{biCC} \end{lemma} \begin{proof} We want to generalize contstruction in \ref{coverheyting} for arbitrary bicartesian closed category. We mimic the construction in \cite{angiuli2022canonicity}. Let $\mathcal{C}$ be a bicartesian closed category and let $(X,A,f)$ and $(Y,B,g)$, we want to construct the exponential object $(Y,B,g)^{(X,A,g)}$. As in \ref{coverheyting} we expect the exponential to mimic $(Y^X,B^C,h)$ where $h: Y^X \to \Gamma(B^C)$; however we know that $(Y^X)$ cannot be the rigth $Set$-component of the exponential. morevoer the constuction of $h$ in this situation is slithely more complex. Let's begin by noticing that the global set functor is a product preserving functor and that, since $\mathcal{C}$ is CC, in $\mathcal{C}$ there is the exponential object $B^A$ with evaluation $ev_\mathcal{C}: B^A \times B \to A$. We can form the composition : \begin{equation} u : \Gamma(A) \times \Gamma (B^A) \xrightarrow{\cong} \Gamma ( A \times B^A) \xrightarrow{\Gamma(ev_\mathcal{C})} \Gamma(B) \end{equation} Now, we take the abstraction of $u$ in $Set$, $\hat{u}: \Gamma(A) \to \Gamma(B)^{\Gamma(A)}$. Consider now the following pullback diagram: % https://q.uiver.app/#q=WzAsNSxbMCwwLCJIIl0sWzAsMiwiXFxHYW1tYShCXkEpIl0sWzEsMywiXFxHYW1tYShCKV57XFxHYW1tYShBKX0iXSxbMiwyLCJcXEdhbW1hKEQpXlgiXSxbMiwwLCJZXlgiXSxbMCwxLCJwXzEiLDJdLFsxLDIsIlxcaGF0e3V9IiwyXSxbMiwzLCIoXFxHYW1tYShEKSleZiIsMl0sWzEsM10sWzQsMywiZ15YIl0sWzAsNCwicF8yIl0sWzAsMywiIiwwLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d \[\begin{tikzcd} H && {Y^X} \\ \\ {\Gamma(B^A)} && {\Gamma(B)^X} \\ & {\Gamma(B)^{\Gamma(A)}} \arrow["{p_2}", from=1-1, to=1-3] \arrow["{p_1}"', from=1-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3] \arrow["{g^X}", from=1-3, to=3-3] \arrow[from=3-1, to=3-3] \arrow["{\hat{u}}"', from=3-1, to=4-2] \arrow["{(\Gamma(B))^f}"', from=4-2, to=3-3] \end{tikzcd}\] Where $(\Gamma (D))^f : \Gamma(B)^{\Gamma(A)} \to \Gamma(D)^X$ is defined by $\mu \to \mu \circ f$ and $g^X: Y^X \to \Gamma(B)$ is defined by $\omega \to g \circ \omega$. We claim $(H,B^A, h := p_1)$ to be the exponenetial object $(X,A,f)^{(Y,B,g)}$. We will prove this by checking that, provided $E = (Z,E,k)$, we have a natural ismoporphism $Cov(\mathcal{C})(E \times A, B)\cong Cov(\mathcal{C})(E, B^A)$\footnote{here we make an abuse of notation setting $A:= (X,A,f),B:=(Y,B,g)$}. Let $(\psi_{Set},\psi_{\mathcal{C}})$ in $Cov(\mathcal{C})(E \times A, B)$ then, $\psi_{Set}: Z \times X \to Y$ and $\psi_\mathcal{C}: E \times A \to B$. Thus, using that $Set$ and $\mathcal{C}$ are cartesian closed, we can take the abstractions $\hat{\psi}_{Set}: Z \to Y^X$ and $\hat{\psi}_{C}: E \to B^A$. Now, consider the following diagram: % https://q.uiver.app/#q=WzAsNixbMSwxLCJIIl0sWzEsMywiXFxHYW1tYShCXkEpIl0sWzMsMywiXFxHYW1tYShEKV5YIl0sWzMsMSwiWV5YIl0sWzAsMCwiWiJdLFswLDIsIlxcR2FtbWEoRSkiXSxbMCwxLCJwXzEiLDJdLFsxLDIsIlxcR2FtbWEoRCleZiBcXGNpcmMgXFxoYXR7dX0iLDJdLFszLDIsImdeWCJdLFswLDMsInBfMiJdLFswLDIsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDMsIlxcaGF0e1xccHNpfV97U2V0fSIsMCx7ImN1cnZlIjotMn1dLFs0LDUsImsiLDJdLFs1LDEsIlxcR2FtbWEoXFxoYXR7XFxwc2l9X3tcXG1hdGhjYWx7Q319KSIsMl0sWzQsMCwiXFxleGlzdCAhIFxccGhpX3tTZXR9IiwxXV0= \[\begin{tikzcd} Z &&& \\ & H && {Y^X} \\ {\Gamma(E)} \\ & {\Gamma(B^A)} && {\Gamma(D)^X} \arrow["{\exists ! \phi_{Set}}"{description}, from=1-1, to=2-2] \arrow["{\hat{\psi}_{Set}}", curve={height=-12pt}, from=1-1, to=2-4] \arrow["k"', from=1-1, to=3-1] \arrow["{p_2}", from=2-2, to=2-4] \arrow["{p_1}"', from=2-2, to=4-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-4] \arrow["{g^X}", from=2-4, to=4-4] \arrow["{\Gamma(\hat{\psi}_{\mathcal{C}})}"', from=3-1, to=4-2] \arrow["{\Gamma(D)^f \circ \hat{u}}"', from=4-2, to=4-4] \end{tikzcd}\] \end{proof} \begin{proposition} The Freyd Cover of a bicartesian closed category extend to an endofunctor % https://q.uiver.app/#q=WzAsOCxbMCwwLCJcXHRleHRiZntiQ0N9Il0sWzIsMCwiXFx0ZXh0YmZ7YkNDfSJdLFswLDEsIlxcbWF0aGNhbHtBfSJdLFsyLDEsIkNvdihcXG1hdGhjYWx7QX0pIl0sWzAsMiwiXFxtYXRoY2Fse0J9Il0sWzIsMiwiQ292KFxcbWF0aGNhbHtCfSkiXSxbMywxLCIoWCxBLGYpIl0sWzMsMiwiKFgsIEZBLCBGZikiXSxbMCwxLCJDb3YoLSkiXSxbMiw0LCJGIiwyXSxbMyw1LCJDbyB2KEYpIl0sWzYsNywiQ292KEYpIl0sWzksMTAsIkNvdigtKSIsMCx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d \[\begin{tikzcd} {\textbf{biCC}} && {\textbf{biCC}} & \\ {\mathcal{A}} && {Cov(\mathcal{A})} & {(X,A,f)} \\ {\mathcal{B}} && {Cov(\mathcal{B})} & {(X, FA, Ff)} \arrow["{Cov(-)}", from=1-1, to=1-3] \arrow[""{name=0, anchor=center, inner sep=0}, "F"', from=2-1, to=3-1] \arrow[""{name=1, anchor=center, inner sep=0}, "{Co v(F)}", from=2-3, to=3-3] \arrow["{Cov(F)}", from=2-4, to=3-4] \arrow["{Cov(-)}", between={0.2}{0.8}, maps to, from=0, to=1] \end{tikzcd}\] we can check that the external square commutes using unicity of abstraction so whe check that $Ev_{Set}\Gamma(D)^f \hat{u} \Gamma()$ \end{proposition} \printbibliography \end{document}