Sinsa/Tesi
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
df9a3121d5a61477b7ff6852e34f43b6a69ad933
Tesi/Tesi.tex
T
Sinsa df9a3121d5 sitemati typo
2026-05-19 15:25:16 +02:00

804 lines
65 KiB
TeX
Raw Blame History

% !TeX spellcheck = en_US
\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
\setcounter{chapter}{-1}
\chapter{Introduction}
\chapter{Freyd Cover}
\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}$-morphism
\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 continuous functor - i.e. preserves small colimits - then the comma category $(F\downarrow G)$ is finitely cocomplete; moreover the forgetful functors are continuous. \\
Analogously if $\mathcal{A}$ and $\mathcal{B}$ are finitely complete categories and $G: \mathcal{A} \to \mathcal{C}$ is continuos - i.e. preserves small limits - then $(F \downarrow G)$ is finitely complete and both forgetful functors are continuos.
\end{theorem}
\begin{proof}
Let's begin by proving the cocomplete case. We will start from completeness of the category and then we will move on to the 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 explicitly both objects: \\
\textbf{Initial Object}: We will construct the initial object of $(F, \downarrow G)$ by using the completeness 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 continuous 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 initial 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 pushouts 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 property 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 commutative:
\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$ being 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 uniqueness of $(u_A,u_B)$ comes almost for free: indeed if there was another arrow $(l,m)$ satisfying 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 forgetful functors are continuous}: the cocontinuity of $\Pi_1, \Pi_2$ arises immediately from the structure of initial object and pushouts of $(F \downarrow G)$. Indeed take the initial 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 continuos. The structure of the proof is completely analog \footnote{Notice that we can also argue that, being $(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 uniqueness is directly inherited by uniqueness 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 actual arrows of $(F \downarrow G)$, indeed:
\begin{align}
Gq_2u = f'Fp_2 \\
Gq_1u = fFp_1
\end{align}
Now, we check that the universal property 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 proceed 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 continuos}: the proof is analogous 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}$ being cocomplete and $F$ being cocontinuos the comma category $(F \downarrow G)$ is cocomplete and that $\Pi_i$ is cocontinuos; moreover we proved the dual result with completeness 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 object $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 coproducts - 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 coproducts 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 omitted \\
\textbf{Binary Products}: Recall that $\mathcal{C}(1_\mathcal{C},-): \mathcal{C} \to Set$ is a continuos 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\pi_x,g\pi_y> := 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 isomorphism, thus $\pi_1 = \mathcal{C}(\_\mathcal{C},-)\pi_A$ and $\pi_2 = \mathcal{C}(\_\mathcal{C},-)\pi_B$ and so the identity 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 respectively 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=WzAsNixbMCwxLCJYIFxcb3BsdXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBIFxcb3BsdXMgQikiXSxbMSwwLCJcXGlvdGFfWCIsMl0sWzIsMCwiXFxpb3RhX1kiXSxbMSwzLCJmIl0sWzIsNCwiZyIsMl0sWzMsNSwiKFxcbWF0aGNhbHtpXzF9KV9cXG1hdGhjYWx7Q30iXSxbNCw1LCIoXFxpb3RhX3syfSlfXFxtYXRoY2Fse0N9IiwyXSxbMCw1LCJcXGV4aXN0cyAhIGYgXFxvcGx1cyBnIl1d&macro_url=https%3A%2F%2Fq.uiver.app%2F%23q%3DWzAsNixbMCwwLCJDb3YoXFxtYXRoY2Fse0F9KSJdLFsyLDAsIkNvdnsoXFxtYXRoY2Fse0J9KX0iXSxbMCwxLCIoWCxBLGYpIl0sWzIsMSwiKFgsRkEsRmYpIl0sWzAsMiwiKFksQixnKSJdLFsyLDIsIihZLEZCLEZnKSJdLFswLDFdLFsyLDMsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMiw0LCIoaCxrKSIsMl0sWzMsNSwiKGgsRmspIl0sWzgsOSwiIiwyLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwibGV2ZWwiOjEsInN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XV0%3D
\[\begin{tikzcd}
& X & {\mathcal{C}(1_\mathcal{C},A)} & \\
{X \oplus Y} &&& {\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["{(\mathcal{\iota}_1)_\mathcal{C}}", 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})_\mathcal{C}}"', from=3-3, to=2-4]
\end{tikzcd}\]
The proof is dual to the proof of binary product and so we omit the calculations. \\
\textbf{Projection is cartesian closed}: the proof of $\Pi_2$ being cartesian closed functor is identical to the proof of $\Pi_1$ being continuos in \ref{completenesscomma}
\end{proof}
\begin{remark}
Notice that this theorem can be generalized for arbitrary comma categories with appropriate assumptions. In fact the construction process of products and coproduct of this proof can be generalized with the same approach we used in the proof of \ref{completenesscomma}.
\end{remark}
\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. Moreover 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 being $\mathcal{H}$ an ordered category if $a \to b$ in non-empty 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 terminal 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 coherence 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}$ which 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 closed 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{remark}[Structure of $Cov(\mathcal{C})(1, A \oplus B)$] \label{global section in cover rmk}
Let $(u,v): 1 \to (X \oplus Y, a \lor b, f \oplus g)$ and consider $u: 1_{Set} \to X \oplus Y$. Since the coproduct in $Set$ is precisely the disjoint union, then $u(\star)$ is either in $X$ or in $Y$. Assume $u(\star) = x_0 = \iota_X(x_0) \in X$ for some $x_0 \in X$, then $(f \oplus g) \circ u = \Gamma v \circ un $ implies $v(\star)= (\iota_1)_\mathcal{C} \circ f (x_0)$. Since this argument is symmetrical if $u(\star) \in Y$ we have the following decomposition:
\[
Cov(\mathcal{C})(1, A \oplus B) \cong Cov(\mathcal{C})(1, A ) \sqcup Cov(\mathcal{C})(1, B)
\]
\end{remark}
\begin{definition}
Let $\mathcal{H}$ be an Heyting Algebra, then we call its Freyd cover the Freyd-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}\label{cover of cc is cc}
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 the construction 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 right $Set$-component of the exponential. The construction of $h$ in this situation is slightly 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 exponential object $(X,A,f)^{(Y,B,g)}$. We will prove this by checking that, provided $E = (Z,E,k)$, we have a natural isomorphism $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)$}. \\
\textbf{Construction of $\Phi: \mathbf{Cov(\mathcal{C})(E \times A, B) \to Cov(\mathcal{C})(E, B^A)}$}: 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}\]
we can check that the external square commutes using unicity of abstraction; so whe check that:
\begin{equation}\label{pullback condition}
Ev_{Set} \circ (g^X \circ \hat{\psi}_{Set} \times \mathrm{id}_X)
\;=\;
Ev_{Set} \circ \bigl((\Gamma B)^f \circ \hat{u} \circ \Gamma(\hat{\psi}_{\mathcal{C}}) \circ k \times \ \mathrm{id}_X\bigr)
\end{equation}
Indeed:
\[
Ev_{Set} \circ (g^X \circ \hat{\psi}_{Set} \times id_X) = Ev_{Set} \circ (g^X \times id_X) \circ (\hat{\psi}_{Set} \times id_X) = g \psi_{Set}
\]
The last equality can be seen using explicit definition of $g^X$; whe have that any $l: z \to Y^X$, $g(l): z \to g(l(z)) \in \Gamma(B)^X$ and so $Ev_{Sev} (g^X \times id_X)$ sends $(l,x)$ to $g(l(x))$. Also $g \circ Ev_{Set}$ sends $(l,x)$ to $g(l(x))$ and thus $Ev_{Set} \circ (g^X \times id_X) = g \circ Ev_{Set}$ and so the equality is justified. Let's move on to the right side of the equation: \\
Let $\psi_2 := \Gamma(\hat{\psi}_{\mathcal{C}})$ and $t := \hat{u} \circ \psi: Z \to {\Gamma B}^{\Gamma A}$. Then the function ${\Gamma B}^f \circ t$ assign to each $z \in Z$ the function $t(z) \circ f: X \to \Gamma B$. Thus the evaluation is comutet as follows:
\[
Ev_{Set} (\Gamma B^f t(z),x) = (t(z) \circ f)(x) = (t(z)f)(x)
\]
this yields to:
\[
Ev_{Set} ( ( \Gamma B^f \circ t) \times id_X ) = Ev_{Set} \circ (t \times f): Z \times X \to \Gamma B
\]
Thus substituting t we obtain:
\begin{align*}
Ev_{Set} \circ \bigl((\Gamma B)^f \circ \hat{u} \circ \Gamma(\hat{\psi}_{\mathcal{C}}) \circ k \times \ \mathrm{id}_X\bigr) & = Ev_{Set} \circ ( (\hat{u} \circ \psi_2 ) \times f) = \\
& = Ev_{Set} \circ ( \hat{u} \times id_{\Gamma A} ) \circ ( \psi_2 \times f )
\end{align*}
Now, recalling that $\hat{u}$ is the abstraction of $\Gamma (Ev_{\mathcal{C}}) \circ \theta : \Gamma A \times \Gamma (B^A) \to \Gamma B$ where $\theta : \Gamma A \times \Gamma (B^A) \to \Gamma (A \times B^A)$ is the canonical isomorphism provided by the fact that the global set functor preserves products we have:
\[
Ev_{Set} \circ (\hat{u} \times id_{\Gamma A}) = \Gamma Ev_{Set} \circ \theta
\]
Therefore:
\[
Ev_{Set} \circ (\hat{u} \times id_{\Gamma A}) \circ (\psi_2 \times f ) = \Gamma (Ev_{Set}) \circ \theta \circ (\psi_2 \times f)
\]
Now, making explicit the definition of $\theta$ we get :
\[
Ev_{Set} \circ ( (\Gamma B^f \circ \hat{u} \circ \psi_2) \times id_X) = \Gamma ( \psi_{\mathcal{C}} ) \circ (k \times f)
\]
Now, the arrow condition on $(\psi_{Set}, \psi_{\mathcal{C}})$ proves the equation \ref{pullback condition}, therefore by the universal property of $H$ there exists a unique $\phi_{Set}: Z \to H$ that makes the pullback diagram commutative. Notice that the universal property of pullbacks ensure us that $(\phi_{Set}, \hat{\psi}_{\mathcal{C}})$ is an element of $Cov(\mathcal{C})(E, B^A)$. Moreover, this construction is unique, hence we have defined a function $\Phi_1: Cov(\mathcal{C})(E \times A, B) \to Cov(\mathcal{C})(E, B^A)$ sending $(\psi_{Set}, \psi_{\mathcal{C}})$ to $(\phi_{Set}, \hat{\psi}_{\mathcal{C}})$. \\
\textbf{Construction of $\mathbf{\Psi:Cov(\mathcal{C})(E, B^A) \to Cov(\mathcal{C})(E \times A, B)}$}: let $(\psi_{Set}, \psi_\mathcal{C})$ in $Cov(\mathcal{C})(E,B^A)$, then the idea is to perform an "inverse construction" with respect to $\Phi$. Let's begin with the $Set$-component. \\
We have $\psi_{Set}: Z \to H$, thus we define $\phi_1 := p_1 \circ \psi_{Set}$ and $\phi_2 := p_2 \circ \psi_{Set}$. Now, we use the exponential structure of $Set$ to define
\[
\bar{\psi}_{Set} := Ev_{Set} \circ (\phi_1 \times id_X) : Z \times X \to Y
\]
Now, we mimic this construction in $\mathcal{C}$ setting
\[
\bar{\psi}_\mathcal{C} := Ev_{C} \circ (\psi_\mathcal{C} \times id_A) : E \times A \to B
\]
We claim that $(\bar{\psi}_{Set},\bar{\psi}_\mathcal{C})$ is an arrow of $Cov(\mathcal{C})$ i.e that
\begin{equation}
g \bar{\psi}_{Set} = \Gamma \bar{\psi}_\mathcal{C} (k \times f) : Z \times X \to \Gamma B
\end{equation}
Now, we begin unfolding the left side of the equation\footnote{we use some identities derived in the last step}:
\begin{align*}
g\bar{\psi}_{Set} = g \circ Ev_{Set} \circ (\phi_1 \times id_X) & = Ev_{Set} \circ ( g^X \times id_X ) \circ (\phi_1 \times id_X) \\
& = Ev_{Set} \circ ((g^X \circ \phi_1) \times id_X)
\end{align*}
Now, by definition $\phi_1$:
\[
g^X \circ \phi_1 = (\Gamma B)^f \circ \hat{u} \circ \psi_2
\]
hence:
\begin{align*}
g\bar{\psi}_{Set} = Ev_{Set} \circ ((\Gamma B^f \circ \hat{u} \circ \Gamma \psi_\mathcal{C} \circ k ) \times id_X )
\end{align*}
Now, with same argument used in \ref{pullback condition}
\[
Ev_{Set} \circ ((\Gamma B^f \circ \hat{u} \circ \Gamma \psi_\mathcal{C} \circ k ) \times id_X ) = Ev_{Set} \circ ((\hat{u} \circ \Gamma \psi_\mathcal{C} \circ k )\times f)
\]
hence substituting:
\begin{align*}
g \bar{\psi}_{Set} = Ev_{Set} \circ (u \times id_\Gamma A ) \circ (\Gamma \psi_\mathcal{C} \circ k , f)
\end{align*}
Now, recalling the definition of $\hat{u}$ and making explicit the canonical isomorphism $\theta$ we get:
\begin{align*}
g \circ \bar{\psi}_{Set} & = \Gamma (Ev_{Set}) \circ \theta \circ (\Gamma \psi_\mathcal{C} k, f) \\
& = \Gamma \bar{\psi}_\mathcal{C} \circ (k ,f)
\end{align*}
Thus, since the universal property of exponentials and pullbacks grant us the unicity of $(\hat{\psi}_{Set}, \hat{\psi}_\mathcal{C})$ then we have successfully constructed a morphism $\Psi:Cov(\mathcal{C})(E, B^A) \to Cov(\mathcal{C})(E \times A, B)$. \\
\textbf{ $\mathbf{\Phi}$ and $\mathbf{\Psi}$ gives a natural isomorphism}: this follows easily by construction. In fact evaluation and abstractions are inverse to each other and, since we are working in $Set$ with the two "projections" of set component the universal property of pullbacks grants us that our functions are inverse each other. Moreover our construction uses only mapping derived from natural isomorphisms - e.g. natural isomorphism of exponential objects in $Set$ and $\mathcal{C}$ and natural isomorphism of pullbacks in $Set$. Therefore our assignment is natural. \\
We proved that there is a natural isomorphism:
\[
Cov(\mathcal{C})(E \times A, B)\cong Cov(\mathcal{C})(E, B^A)
\]
And so the, since the functor $(-)^A$ is right adjoint to $(-) \times A$, then our candidate $(H,B^A,h)$ is indeed the exponential object. Thus $Cov(\mathcal{C})$ is cartesian closed and we are done.
(AGGIUNGERE CONTI)
\end{proof}
\begin{remark}
Notice that the exponential construction in \ref{cover of cc is cc} agrees with exponential construction in \ref{coverheyting} if $\mathcal{C}$ is an ordered category
\end{remark}
\begin{proposition}
The Freyd Cover of a bicartesian closed category extend to an endofunctor
% https://q.uiver.app/#q=WzAsNixbMCwwLCJcXHRleHRiZntiQ0N9Il0sWzIsMCwiXFx0ZXh0YmZ7YkNDfSJdLFswLDEsIlxcbWF0aGNhbHtBfSJdLFsyLDEsIkNvdihcXG1hdGhjYWx7QX0pIl0sWzAsMiwiXFxtYXRoY2Fse0J9Il0sWzIsMiwiQ292KFxcbWF0aGNhbHtCfSkiXSxbMCwxLCJDb3YoLSkiXSxbMiw0LCJGIiwyXSxbMyw1LCJDbyB2KEYpIl0sWzcsOCwiQ292KC0pIiwwLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwibGV2ZWwiOjEsInN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XV0=
\[\begin{tikzcd}
{\textbf{biCC}} && {\textbf{biCC}} \\
{\mathcal{A}} && {Cov(\mathcal{A})} \\
{\mathcal{B}} && {Cov(\mathcal{B})}
\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(-)}", between={0.2}{0.8}, maps to, from=0, to=1]
\end{tikzcd}\]
where:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJDb3YoXFxtYXRoY2Fse0F9KSJdLFsyLDAsIkNvdnsoXFxtYXRoY2Fse0J9KX0iXSxbMCwxLCIoWCxBLGYpIl0sWzIsMSwiKFgsRkEsRmYpIl0sWzAsMiwiKFksQixnKSJdLFsyLDIsIihZLEZCLEZnKSJdLFswLDEsIkNvdihGKSJdLFsyLDMsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMiw0LCIoaCxrKSIsMl0sWzMsNSwiKGgsRmspIl0sWzgsOSwiIiwyLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwibGV2ZWwiOjEsInN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XV0=&macro_url=https%3A%2F%2Fq.uiver.app%2F%23q%3DWzAsNixbMCwwLCJDb3YoXFxtYXRoY2Fse0F9KSJdLFsyLDAsIkNvdnsoXFxtYXRoY2Fse0J9KX0iXSxbMCwxLCIoWCxBLGYpIl0sWzIsMSwiKFgsRkEsRmYpIl0sWzAsMiwiKFksQixnKSJdLFsyLDIsIihZLEZCLEZnKSJdLFswLDFdLFsyLDMsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbMiw0LCIoaCxrKSIsMl0sWzMsNSwiKGgsRmspIl0sWzgsOSwiIiwyLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwibGV2ZWwiOjEsInN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XV0%3D
\[\begin{tikzcd}
{Cov(\mathcal{A})} && {Cov{(\mathcal{B})}} \\
{(X,A,f)} && {(X,FA,F\cdot f)} \\
{(Y,B,g)} && {(Y,FB,F \cdot g)}
\arrow["{Cov(F)}", from=1-1, to=1-3]
\arrow[maps to, from=2-1, to=2-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{(h,k)}"', from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{(h,Fk)}", from=2-3, to=3-3]
\arrow[between={0.2}{0.8}, maps to, from=0, to=1]
\end{tikzcd}\]
where $F\cdot f: X \to \Gamma (FA)$ is the set function defined sending $x \in X$ into the global setion of $FA$ given by $F( f(x)) : 1_\mathcal{B} \to FA$
\end{proposition}
\begin{proof}
By lemma \ref{cover of cc is cc} $Cov(-)$ extend to a class function from \textbf{biCC} to itself. Then notice that the action of $Cov(-)$ over arrows of \textbf{biCC} is well defined since the commutativity condition of the arrow is preserved under the action of $F$. Indeed by definition of $F \cdot f$ and $F \cdot g$ we have:
\[
(F \cdot g) \circ h = F(\Gamma k) \circ (F \cdot f)
\]
And so for $F: A \to B$ we proved $Cov(F): Cov(\mathcal{A}) \to Cov(\mathcal{B})$ is a well defined functor. Moreover, clearly $Cov(Id_\mathcal{A})= Id_{Cov(\mathcal{A})}$ and by definition of $F \cdot f$ taking $F: \mathcal{A} \to \mathcal{B}$ and $G: \mathcal{B} \to \mathcal{C}$ we have that $Cov(G \cdot F) = Cov(G) \cdot Cov(F)$. Thus $Cov(-): \textbf{biCC} \to \textbf{biCC}$ is a well defined endofunctor
\end{proof}
\begin{corollary}
Taking posettal reflection of a lattice - i.e. an ordered bicartesian closed category - gives rise to an endofunctor:
\[
Pcov(-): \textbf{bLat} \to \textbf{bLat}
\]
where $Pcov(-) := Pos \circ Cov (-) : \textbf{bLat} \to\textbf{bLat}$ and \textbf{bLat} is the category of bounded lattices - i.e. lattice with top and bottom objects - with lattice homomorphisms as arrows.
\end{corollary}
\begin{proof}
By lemma \ref{cover of bicartesian} the cover of a lattice has a bicartesian structure and by lemma \ref{cover of cc is cc} the cover of a lattice is also a cartesian closed category. Therefore we are done, since the posettal reflection of a bicartesian closed category is a bounded lattice (the posettal reflection preserves bicartesian closed structure of the category)
\end{proof}
\section{Application to Logic}
After defining the construction of Freyd Cover and proving some basic property of this construction we are ready to use the categorical property of $Cov(-)$ to show some logical property of intuitionistic logic. In this section we will prove categorically that the propositional logic satisfy the disjunction property using the Freyd Cover construction.
\begin{theorem}
Let the following disjunction $\phi \lor \psi$ be derivable in the intuitionistic propositional logic. Then either $\phi$ or $\psi$ is derivable.
\end{theorem}
\begin{proof} \, \\
\textbf{Idea}: We will apply our construction to the Lindembaum-Tarski algebra of the initial intuitionistic propositional logic $\mathcal{T}_0$. Notice that the projection $\Pi_2: Cov(\mathcal{A}_i(\mathcal{T}_0)) \to \mathcal{A}_i(\mathcal{T}_0)$ "preserves" the Lindembaum component of element of $Cov(\mathcal{A}_i(\mathcal{T}_0))$,therefore a clever model build upon $Cov(\mathcal{A}_i(\mathcal{T}_0))$ respects the categorical semantics of $\mathcal{T}_0$. We will use this property to construct, from the fact that $\phi \lor \psi$ holds, a global section of $\phi$ or $\psi$, proving the disjunction property. \\
\textbf{Proof}: Let $\mathcal{T}_0$ be the initial intuitionistic propositional theory and consider the Lindembaum-Tarski algebra $\mathcal{A}_i(\mathcal{T}_0)$. Notice that $Pcov(\mathcal{A}_i(\mathcal{T}_0))$is an heyting algebra, so we can define a model
\[
\nu : Frm(\mathcal{T}_0) \to Pcov(\mathcal{A}_i(\mathcal{T}_0))
\]
in the following way: let $A$ be a propositional variable, then
\[
A \to \nu(A)= [(X_A, [A], e_A)]
\]
where $X_A$ is the terminal object in $Set$ if $1 \leq_{\mathcal{A}_i(\mathcal{T}_0)} [A]$ and initial otherwise:
\[
X_A := \{ x = 0 | 1 \leq_{\mathcal{A}_i(\mathcal{T}_0)} [A] \}
\]
notice that $[(X_A,[A],e_A)]$ is a well defined element of $Pcov(\mathcal{A}_i(\mathcal{T}_0))$. In fact if $A$ is the top in $\mathcal{A}_i(\mathcal{T}_0)$ then the set global section of the class $[A]$ is terminal and so $e_A$ is uniquely defined. Otherwise $X_A$ is initial in $Set$ and thus again $e_A$ is uniquely defined. Now, this definition can be extended inductively by lifting the Lindembaum-Tarski evaluation to the Freyd Cover, namely by setting $\nu(\psi \land psi) = \nu (\psi) \times \nu (\psi)$, $\nu (\psi \lor \psi) = \nu(\phi) \oplus \nu(\psi)$ and $\nu(\phi \to \psi)= \nu(\psi)^{\nu(\phi)}$. Therefore for an arbitrary formula $\phi$ we have:
\[
\nu(\phi) = [(X_\phi, [\phi], e_\phi)]
\]
for some $X_\phi$ in $Set$ and $e_\phi : X_\phi \to \Gamma [\phi]$. Notice that in this model the evaluation of a propositional variable $A$ and $\neg A$ is neither the top or the bottom (this follows immediately by construction). \\
Let $\phi \lor \psi$ be a tautology in $\mathcal{T}_0$, therefore \[\nu(\phi \lor \psi) = 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} = [(1_{Set}, 1_{\mathcal{A}_i(\mathcal{T}_0)},un)]
\]
Now, since $\nu (\phi \lor \psi)= \nu(\phi) \oplus \nu(\psi)$ there exists a global section $g: 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to [(X_\phi , [\phi] , e_\phi)] \oplus [(X_\psi , [\psi], e_\psi)]$.
By remark \ref{global section in cover rmk} $g = (g_1,g_2): 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to \nu(\phi)$ or $g = (g_1,g_2): 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to \nu(\psi)$. Now, in the first case $e_\phi (g_1(\star)) \in \Gamma [\phi]$ hence $\phi$ is provable in the logic. In the second case $e_\psi (g_1(\star)) \in \Gamma [\psi]$ and so $\psi$ is provable in the logic. Thus the disjunction property is proved and so we are done.$e_\phi (g_1(\star)) \in \Gamma [\phi]$
\end{proof}
\printbibliography
\end{document}
Reference in New Issue View Git Blame Copy Permalink