diff --git a/Bibliografia.bib b/Bibliografia.bib
new file mode 100644
index 0000000..1829299
--- /dev/null
+++ b/Bibliografia.bib
@@ -0,0 +1,5 @@
+@article{angiuli2022canonicity,
+ title={Canonicity for simple types via gluing},
+ author={Angiuli, Carlo},
+ year={2022}
+}
diff --git a/Tesi.aux b/Tesi.aux
new file mode 100644
index 0000000..e7e7cd0
--- /dev/null
+++ b/Tesi.aux
@@ -0,0 +1,25 @@
+\relax
+\abx@aux@refcontext{nty/global//global/global/global}
+\@writefile{toc}{\contentsline {section}{\numberline {0.1}Introduction}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {0.2}Freyd cover of a category}{2}{}\protected@file@percent }
+\newlabel{completenesscomma}{{0.2.3}{3}{}{definition.0.2.3}{}}
+\newlabel{push_1}{{1}{4}{}{equation.0.1}{}}
+\newlabel{def-u}{{2}{5}{}{equation.0.2}{}}
+\newlabel{x'y'}{{3}{6}{}{equation.0.3}{}}
+\newlabel{x''y''}{{4}{6}{}{equation.0.4}{}}
+\newlabel{pushoutarrinAB}{{5}{6}{}{equation.0.5}{}}
+\newlabel{goalpush}{{6}{6}{}{equation.0.6}{}}
+\newlabel{uAuBarrow}{{7}{7}{}{equation.0.7}{}}
+\newlabel{pull}{{10}{10}{}{equation.0.10}{}}
+\newlabel{pullstart}{{11}{10}{}{equation.0.11}{}}
+\newlabel{cover of bicartesian}{{0.2.6}{11}{}{definition.0.2.6}{}}
+\newlabel{prodgoal}{{13}{12}{}{equation.0.13}{}}
+\newlabel{coverheyting}{{0.2}{14}{}{definition.0.2.8}{}}
+\abx@aux@cite{0}{angiuli2022canonicity}
+\abx@aux@segm{0}{0}{angiuli2022canonicity}
+\newlabel{exp goal}{{14}{15}{}{equation.0.14}{}}
+\newlabel{cover of cc is cc}{{0.2.12}{15}{}{definition.0.2.12}{}}
+\newlabel{pullback condition}{{16}{17}{}{equation.0.16}{}}
+\abx@aux@read@bbl@mdfivesum{A692FE2EF8541C6E6F38713971A59175}
+\abx@aux@defaultrefcontext{0}{angiuli2022canonicity}{nty/global//global/global/global}
+\gdef \@abspage@last{21}
diff --git a/Tesi.bbl b/Tesi.bbl
new file mode 100644
index 0000000..b9aa71e
--- /dev/null
+++ b/Tesi.bbl
@@ -0,0 +1,48 @@
+% $ biblatex auxiliary file $
+% $ biblatex bbl format version 3.3 $
+% Do not modify the above lines!
+%
+% This is an auxiliary file used by the 'biblatex' package.
+% This file may safely be deleted. It will be recreated by
+% biber as required.
+%
+\begingroup
+\makeatletter
+\@ifundefined{ver@biblatex.sty}
+ {\@latex@error
+ {Missing 'biblatex' package}
+ {The bibliography requires the 'biblatex' package.}
+ \aftergroup\endinput}
+ {}
+\endgroup
+
+
+\refsection{0}
+ \datalist[entry]{nty/global//global/global/global}
+ \entry{angiuli2022canonicity}{article}{}{}
+ \name{author}{1}{}{%
+ {{hash=ab4a713b0ee991d87b0eeda400ad210a}{%
+ family={Angiuli},
+ familyi={A\bibinitperiod},
+ given={Carlo},
+ giveni={C\bibinitperiod}}}%
+ }
+ \strng{namehash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{fullhash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{fullhashraw}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{bibnamehash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{authorbibnamehash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{authornamehash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{authorfullhash}{ab4a713b0ee991d87b0eeda400ad210a}
+ \strng{authorfullhashraw}{ab4a713b0ee991d87b0eeda400ad210a}
+ \field{sortinit}{A}
+ \field{sortinithash}{2f401846e2029bad6b3ecc16d50031e2}
+ \field{labelnamesource}{author}
+ \field{labeltitlesource}{title}
+ \field{title}{Canonicity for simple types via gluing}
+ \field{year}{2022}
+ \endentry
+ \enddatalist
+\endrefsection
+\endinput
+
diff --git a/Tesi.bcf b/Tesi.bcf
new file mode 100644
index 0000000..c02b71b
--- /dev/null
+++ b/Tesi.bcf
@@ -0,0 +1,2418 @@
+
+
+
+
+
+ output_encoding
+ utf8
+
+
+ input_encoding
+ utf8
+
+
+ debug
+ 0
+
+
+ mincrossrefs
+ 2
+
+
+ minxrefs
+ 2
+
+
+ sortcase
+ 1
+
+
+ sortupper
+ 1
+
+
+
+
+
+
+ alphaothers
+ +
+
+
+ extradatecontext
+ labelname
+ labeltitle
+
+
+ labelalpha
+ 0
+
+
+ labelnamespec
+ shortauthor
+ author
+ shorteditor
+ editor
+ translator
+
+
+ labeltitle
+ 0
+
+
+ labeltitlespec
+ shorttitle
+ title
+ maintitle
+
+
+ labeltitleyear
+ 0
+
+
+ labeldateparts
+ 0
+
+
+ labeldatespec
+ date
+ year
+ eventdate
+ origdate
+ urldate
+ nodate
+
+
+ julian
+ 0
+
+
+ gregorianstart
+ 1582-10-15
+
+
+ maxalphanames
+ 3
+
+
+ maxbibnames
+ 3
+
+
+ maxcitenames
+ 3
+
+
+ maxsortnames
+ 3
+
+
+ maxitems
+ 3
+
+
+ minalphanames
+ 1
+
+
+ minbibnames
+ 1
+
+
+ mincitenames
+ 1
+
+
+ minsortnames
+ 1
+
+
+ minitems
+ 1
+
+
+ nohashothers
+ 0
+
+
+ noroman
+ 0
+
+
+ nosortothers
+ 0
+
+
+ pluralothers
+ 0
+
+
+ singletitle
+ 0
+
+
+ skipbib
+ 0
+
+
+ skipbiblist
+ 0
+
+
+ skiplab
+ 0
+
+
+ sortalphaothers
+ +
+
+
+ sortlocale
+ english
+
+
+ sortingtemplatename
+ nty
+
+
+ sortsets
+ 0
+
+
+ uniquelist
+ false
+
+
+ uniquename
+ false
+
+
+ uniqueprimaryauthor
+ 0
+
+
+ uniquetitle
+ 0
+
+
+ uniquebaretitle
+ 0
+
+
+ uniquework
+ 0
+
+
+ useprefix
+ 0
+
+
+ useafterword
+ 1
+
+
+ useannotator
+ 1
+
+
+ useauthor
+ 1
+
+
+ usebookauthor
+ 1
+
+
+ usecommentator
+ 1
+
+
+ useeditor
+ 1
+
+
+ useeditora
+ 1
+
+
+ useeditorb
+ 1
+
+
+ useeditorc
+ 1
+
+
+ useforeword
+ 1
+
+
+ useholder
+ 1
+
+
+ useintroduction
+ 1
+
+
+ usenamea
+ 1
+
+
+ usenameb
+ 1
+
+
+ usenamec
+ 1
+
+
+ usetranslator
+ 0
+
+
+ useshortauthor
+ 1
+
+
+ useshorteditor
+ 1
+
+
+
+
+
+ extradatecontext
+ labelname
+ labeltitle
+
+
+ labelalpha
+ 0
+
+
+ labelnamespec
+ shortauthor
+ author
+ shorteditor
+ editor
+ translator
+
+
+ labeltitle
+ 0
+
+
+ labeltitlespec
+ shorttitle
+ title
+ maintitle
+
+
+ labeltitleyear
+ 0
+
+
+ labeldateparts
+ 0
+
+
+ labeldatespec
+ date
+ year
+ eventdate
+ origdate
+ urldate
+ nodate
+
+
+ maxalphanames
+ 3
+
+
+ maxbibnames
+ 3
+
+
+ maxcitenames
+ 3
+
+
+ maxsortnames
+ 3
+
+
+ maxitems
+ 3
+
+
+ minalphanames
+ 1
+
+
+ minbibnames
+ 1
+
+
+ mincitenames
+ 1
+
+
+ minsortnames
+ 1
+
+
+ minitems
+ 1
+
+
+ nohashothers
+ 0
+
+
+ noroman
+ 0
+
+
+ nosortothers
+ 0
+
+
+ singletitle
+ 0
+
+
+ skipbib
+ 0
+
+
+ skipbiblist
+ 0
+
+
+ skiplab
+ 0
+
+
+ uniquelist
+ false
+
+
+ uniquename
+ false
+
+
+ uniqueprimaryauthor
+ 0
+
+
+ uniquetitle
+ 0
+
+
+ uniquebaretitle
+ 0
+
+
+ uniquework
+ 0
+
+
+ useprefix
+ 0
+
+
+ useafterword
+ 1
+
+
+ useannotator
+ 1
+
+
+ useauthor
+ 1
+
+
+ usebookauthor
+ 1
+
+
+ usecommentator
+ 1
+
+
+ useeditor
+ 1
+
+
+ useeditora
+ 1
+
+
+ useeditorb
+ 1
+
+
+ useeditorc
+ 1
+
+
+ useforeword
+ 1
+
+
+ useholder
+ 1
+
+
+ useintroduction
+ 1
+
+
+ usenamea
+ 1
+
+
+ usenameb
+ 1
+
+
+ usenamec
+ 1
+
+
+ usetranslator
+ 0
+
+
+ useshortauthor
+ 1
+
+
+ useshorteditor
+ 1
+
+
+
+
+ datamodel
+ labelalphanametemplate
+ labelalphatemplate
+ inheritance
+ translit
+ uniquenametemplate
+ namehashtemplate
+ sortingnamekeytemplate
+ sortingtemplate
+ extradatespec
+ extradatecontext
+ labelnamespec
+ labeltitlespec
+ labeldatespec
+ controlversion
+ alphaothers
+ sortalphaothers
+ presort
+ citepagerange
+ texencoding
+ bibencoding
+ sortingtemplatename
+ sortlocale
+ language
+ autolang
+ langhook
+ indexing
+ hyperref
+ backrefsetstyle
+ block
+ pagetracker
+ citecounter
+ citetracker
+ ibidtracker
+ idemtracker
+ opcittracker
+ loccittracker
+ labeldate
+ labeltime
+ dateera
+ date
+ time
+ eventdate
+ eventtime
+ origdate
+ origtime
+ urldate
+ urltime
+ alldatesusetime
+ alldates
+ alltimes
+ gregorianstart
+ autocite
+ notetype
+ uniquelist
+ uniquename
+ refsection
+ refsegment
+ citereset
+ sortlos
+ babel
+ datelabel
+ backrefstyle
+ arxiv
+ familyinits
+ giveninits
+ prefixinits
+ suffixinits
+ useafterword
+ useannotator
+ useauthor
+ usebookauthor
+ usecommentator
+ useeditor
+ useeditora
+ useeditorb
+ useeditorc
+ useforeword
+ useholder
+ useintroduction
+ usenamea
+ usenameb
+ usenamec
+ usetranslator
+ useshortauthor
+ useshorteditor
+ debug
+ loadfiles
+ safeinputenc
+ sortcase
+ sortupper
+ terseinits
+ abbreviate
+ dateabbrev
+ clearlang
+ sortcites
+ sortsets
+ backref
+ backreffloats
+ trackfloats
+ parentracker
+ labeldateusetime
+ datecirca
+ dateuncertain
+ dateusetime
+ eventdateusetime
+ origdateusetime
+ urldateusetime
+ julian
+ datezeros
+ timezeros
+ timezones
+ seconds
+ autopunct
+ punctfont
+ labelnumber
+ labelalpha
+ labeltitle
+ labeltitleyear
+ labeldateparts
+ pluralothers
+ nohashothers
+ nosortothers
+ noroman
+ singletitle
+ uniquetitle
+ uniquebaretitle
+ uniquework
+ uniqueprimaryauthor
+ defernumbers
+ locallabelwidth
+ bibwarn
+ useprefix
+ skipbib
+ skipbiblist
+ skiplab
+ dataonly
+ defernums
+ firstinits
+ sortfirstinits
+ sortgiveninits
+ labelyear
+ isbn
+ url
+ doi
+ eprint
+ related
+ subentry
+ bibtexcaseprotection
+ mincrossrefs
+ minxrefs
+ maxnames
+ minnames
+ maxbibnames
+ minbibnames
+ maxcitenames
+ mincitenames
+ maxsortnames
+ minsortnames
+ maxitems
+ minitems
+ maxalphanames
+ minalphanames
+ maxparens
+ dateeraauto
+
+
+ alphaothers
+ sortalphaothers
+ presort
+ indexing
+ citetracker
+ ibidtracker
+ idemtracker
+ opcittracker
+ loccittracker
+ uniquelist
+ uniquename
+ familyinits
+ giveninits
+ prefixinits
+ suffixinits
+ useafterword
+ useannotator
+ useauthor
+ usebookauthor
+ usecommentator
+ useeditor
+ useeditora
+ useeditorb
+ useeditorc
+ useforeword
+ useholder
+ useintroduction
+ usenamea
+ usenameb
+ usenamec
+ usetranslator
+ useshortauthor
+ useshorteditor
+ terseinits
+ abbreviate
+ dateabbrev
+ clearlang
+ labelnumber
+ labelalpha
+ labeltitle
+ labeltitleyear
+ labeldateparts
+ nohashothers
+ nosortothers
+ noroman
+ singletitle
+ uniquetitle
+ uniquebaretitle
+ uniquework
+ uniqueprimaryauthor
+ useprefix
+ skipbib
+ skipbiblist
+ skiplab
+ dataonly
+ skiplos
+ labelyear
+ isbn
+ url
+ doi
+ eprint
+ related
+ subentry
+ bibtexcaseprotection
+ labelalphatemplate
+ translit
+ sortexclusion
+ sortinclusion
+ extradatecontext
+ labelnamespec
+ labeltitlespec
+ labeldatespec
+ maxnames
+ minnames
+ maxbibnames
+ minbibnames
+ maxcitenames
+ mincitenames
+ maxsortnames
+ minsortnames
+ maxitems
+ minitems
+ maxalphanames
+ minalphanames
+
+
+ noinherit
+ nametemplates
+ labelalphanametemplatename
+ uniquenametemplatename
+ namehashtemplatename
+ sortingnamekeytemplatename
+ presort
+ indexing
+ citetracker
+ ibidtracker
+ idemtracker
+ opcittracker
+ loccittracker
+ uniquelist
+ uniquename
+ familyinits
+ giveninits
+ prefixinits
+ suffixinits
+ useafterword
+ useannotator
+ useauthor
+ usebookauthor
+ usecommentator
+ useeditor
+ useeditora
+ useeditorb
+ useeditorc
+ useforeword
+ useholder
+ useintroduction
+ usenamea
+ usenameb
+ usenamec
+ usetranslator
+ useshortauthor
+ useshorteditor
+ terseinits
+ abbreviate
+ dateabbrev
+ clearlang
+ labelnumber
+ labelalpha
+ labeltitle
+ labeltitleyear
+ labeldateparts
+ nohashothers
+ nosortothers
+ noroman
+ singletitle
+ uniquetitle
+ uniquebaretitle
+ uniquework
+ uniqueprimaryauthor
+ useprefix
+ skipbib
+ skipbiblist
+ skiplab
+ dataonly
+ skiplos
+ isbn
+ url
+ doi
+ eprint
+ related
+ subentry
+ bibtexcaseprotection
+ maxnames
+ minnames
+ maxbibnames
+ minbibnames
+ maxcitenames
+ mincitenames
+ maxsortnames
+ minsortnames
+ maxitems
+ minitems
+ maxalphanames
+ minalphanames
+
+
+ nametemplates
+ labelalphanametemplatename
+ uniquenametemplatename
+ namehashtemplatename
+ sortingnamekeytemplatename
+ uniquelist
+ uniquename
+ familyinits
+ giveninits
+ prefixinits
+ suffixinits
+ terseinits
+ nohashothers
+ nosortothers
+ useprefix
+
+
+ nametemplates
+ labelalphanametemplatename
+ uniquenametemplatename
+ namehashtemplatename
+ sortingnamekeytemplatename
+ uniquename
+ familyinits
+ giveninits
+ prefixinits
+ suffixinits
+ terseinits
+ useprefix
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ prefix
+ family
+
+
+
+
+ shorthand
+ label
+ labelname
+ labelname
+
+
+ year
+
+
+
+
+
+ labelyear
+ year
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ prefix
+ family
+ given
+
+
+
+ family
+ given
+ prefix
+ suffix
+
+
+
+
+ prefix
+ family
+
+
+ given
+
+
+ suffix
+
+
+ prefix
+
+
+ mm
+
+
+
+ sf,sm,sn,pf,pm,pn,pp
+ family,given,prefix,suffix
+ boolean,integer,string,xml
+ default,transliteration,transcription,translation
+
+
+ article
+ artwork
+ audio
+ bibnote
+ book
+ bookinbook
+ booklet
+ collection
+ commentary
+ customa
+ customb
+ customc
+ customd
+ custome
+ customf
+ dataset
+ inbook
+ incollection
+ inproceedings
+ inreference
+ image
+ jurisdiction
+ legal
+ legislation
+ letter
+ manual
+ misc
+ movie
+ music
+ mvcollection
+ mvreference
+ mvproceedings
+ mvbook
+ online
+ patent
+ performance
+ periodical
+ proceedings
+ reference
+ report
+ review
+ set
+ software
+ standard
+ suppbook
+ suppcollection
+ suppperiodical
+ thesis
+ unpublished
+ video
+ xdata
+
+
+ sortyear
+ volume
+ volumes
+ abstract
+ addendum
+ annotation
+ booksubtitle
+ booktitle
+ booktitleaddon
+ chapter
+ edition
+ eid
+ entrysubtype
+ eprintclass
+ eprinttype
+ eventtitle
+ eventtitleaddon
+ gender
+ howpublished
+ indexsorttitle
+ indextitle
+ isan
+ isbn
+ ismn
+ isrn
+ issn
+ issue
+ issuesubtitle
+ issuetitle
+ issuetitleaddon
+ iswc
+ journalsubtitle
+ journaltitle
+ journaltitleaddon
+ label
+ langid
+ langidopts
+ library
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ nameaddon
+ note
+ number
+ origtitle
+ pagetotal
+ part
+ relatedstring
+ relatedtype
+ reprinttitle
+ series
+ shorthandintro
+ subtitle
+ title
+ titleaddon
+ usera
+ userb
+ userc
+ userd
+ usere
+ userf
+ venue
+ version
+ shorthand
+ shortjournal
+ shortseries
+ shorttitle
+ sorttitle
+ sortshorthand
+ sortkey
+ presort
+ institution
+ lista
+ listb
+ listc
+ listd
+ liste
+ listf
+ location
+ organization
+ origlocation
+ origpublisher
+ publisher
+ afterword
+ annotator
+ author
+ bookauthor
+ commentator
+ editor
+ editora
+ editorb
+ editorc
+ foreword
+ holder
+ introduction
+ namea
+ nameb
+ namec
+ translator
+ shortauthor
+ shorteditor
+ sortname
+ authortype
+ editoratype
+ editorbtype
+ editorctype
+ editortype
+ bookpagination
+ nameatype
+ namebtype
+ namectype
+ pagination
+ pubstate
+ type
+ language
+ origlanguage
+ crossref
+ xref
+ date
+ endyear
+ year
+ month
+ day
+ hour
+ minute
+ second
+ timezone
+ yeardivision
+ endmonth
+ endday
+ endhour
+ endminute
+ endsecond
+ endtimezone
+ endyeardivision
+ eventdate
+ eventendyear
+ eventyear
+ eventmonth
+ eventday
+ eventhour
+ eventminute
+ eventsecond
+ eventtimezone
+ eventyeardivision
+ eventendmonth
+ eventendday
+ eventendhour
+ eventendminute
+ eventendsecond
+ eventendtimezone
+ eventendyeardivision
+ origdate
+ origendyear
+ origyear
+ origmonth
+ origday
+ orighour
+ origminute
+ origsecond
+ origtimezone
+ origyeardivision
+ origendmonth
+ origendday
+ origendhour
+ origendminute
+ origendsecond
+ origendtimezone
+ origendyeardivision
+ urldate
+ urlendyear
+ urlyear
+ urlmonth
+ urlday
+ urlhour
+ urlminute
+ urlsecond
+ urltimezone
+ urlyeardivision
+ urlendmonth
+ urlendday
+ urlendhour
+ urlendminute
+ urlendsecond
+ urlendtimezone
+ urlendyeardivision
+ doi
+ eprint
+ file
+ verba
+ verbb
+ verbc
+ url
+ xdata
+ ids
+ entryset
+ related
+ keywords
+ options
+ relatedoptions
+ pages
+ execute
+
+
+ abstract
+ annotation
+ authortype
+ bookpagination
+ crossref
+ day
+ doi
+ eprint
+ eprintclass
+ eprinttype
+ endday
+ endhour
+ endminute
+ endmonth
+ endsecond
+ endtimezone
+ endyear
+ endyeardivision
+ entryset
+ entrysubtype
+ execute
+ file
+ gender
+ hour
+ ids
+ indextitle
+ indexsorttitle
+ isan
+ ismn
+ iswc
+ keywords
+ label
+ langid
+ langidopts
+ library
+ lista
+ listb
+ listc
+ listd
+ liste
+ listf
+ minute
+ month
+ namea
+ nameb
+ namec
+ nameatype
+ namebtype
+ namectype
+ nameaddon
+ options
+ origday
+ origendday
+ origendhour
+ origendminute
+ origendmonth
+ origendsecond
+ origendtimezone
+ origendyear
+ origendyeardivision
+ orighour
+ origminute
+ origmonth
+ origsecond
+ origtimezone
+ origyear
+ origyeardivision
+ origlocation
+ origpublisher
+ origtitle
+ pagination
+ presort
+ related
+ relatedoptions
+ relatedstring
+ relatedtype
+ second
+ shortauthor
+ shorteditor
+ shorthand
+ shorthandintro
+ shortjournal
+ shortseries
+ shorttitle
+ sortkey
+ sortname
+ sortshorthand
+ sorttitle
+ sortyear
+ timezone
+ url
+ urlday
+ urlendday
+ urlendhour
+ urlendminute
+ urlendmonth
+ urlendsecond
+ urlendtimezone
+ urlendyear
+ urlhour
+ urlminute
+ urlmonth
+ urlsecond
+ urltimezone
+ urlyear
+ usera
+ userb
+ userc
+ userd
+ usere
+ userf
+ verba
+ verbb
+ verbc
+ xdata
+ xref
+ year
+ yeardivision
+
+
+ set
+ entryset
+
+
+ article
+ addendum
+ annotator
+ author
+ commentator
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ eid
+ issn
+ issue
+ issuetitle
+ issuesubtitle
+ issuetitleaddon
+ journalsubtitle
+ journaltitle
+ journaltitleaddon
+ language
+ note
+ number
+ origlanguage
+ pages
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ version
+ volume
+
+
+ bibnote
+ note
+
+
+ book
+ author
+ addendum
+ afterword
+ annotator
+ chapter
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ eid
+ foreword
+ introduction
+ isbn
+ language
+ location
+ maintitle
+ maintitleaddon
+ mainsubtitle
+ note
+ number
+ origlanguage
+ pages
+ pagetotal
+ part
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ mvbook
+ addendum
+ afterword
+ annotator
+ author
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ foreword
+ introduction
+ isbn
+ language
+ location
+ note
+ number
+ origlanguage
+ pagetotal
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ inbook
+ bookinbook
+ suppbook
+ addendum
+ afterword
+ annotator
+ author
+ booktitle
+ bookauthor
+ booksubtitle
+ booktitleaddon
+ chapter
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ eid
+ foreword
+ introduction
+ isbn
+ language
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ note
+ number
+ origlanguage
+ part
+ publisher
+ pages
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ booklet
+ addendum
+ author
+ chapter
+ editor
+ editortype
+ eid
+ howpublished
+ language
+ location
+ note
+ pages
+ pagetotal
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+
+
+ collection
+ reference
+ addendum
+ afterword
+ annotator
+ chapter
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ eid
+ foreword
+ introduction
+ isbn
+ language
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ note
+ number
+ origlanguage
+ pages
+ pagetotal
+ part
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ mvcollection
+ mvreference
+ addendum
+ afterword
+ annotator
+ author
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ foreword
+ introduction
+ isbn
+ language
+ location
+ note
+ number
+ origlanguage
+ publisher
+ pubstate
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ incollection
+ suppcollection
+ inreference
+ addendum
+ afterword
+ annotator
+ author
+ booksubtitle
+ booktitle
+ booktitleaddon
+ chapter
+ commentator
+ edition
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ eid
+ foreword
+ introduction
+ isbn
+ language
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ note
+ number
+ origlanguage
+ pages
+ part
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ translator
+ volume
+ volumes
+
+
+ dataset
+ addendum
+ author
+ edition
+ editor
+ editortype
+ language
+ location
+ note
+ number
+ organization
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ type
+ version
+
+
+ manual
+ addendum
+ author
+ chapter
+ edition
+ editor
+ editortype
+ eid
+ isbn
+ language
+ location
+ note
+ number
+ organization
+ pages
+ pagetotal
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ type
+ version
+
+
+ misc
+ software
+ addendum
+ author
+ editor
+ editortype
+ howpublished
+ language
+ location
+ note
+ organization
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+ version
+
+
+ online
+ addendum
+ author
+ editor
+ editortype
+ language
+ note
+ organization
+ pubstate
+ subtitle
+ title
+ titleaddon
+ version
+
+
+ patent
+ addendum
+ author
+ holder
+ location
+ note
+ number
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+ version
+
+
+ periodical
+ addendum
+ editor
+ editora
+ editorb
+ editorc
+ editortype
+ editoratype
+ editorbtype
+ editorctype
+ issn
+ issue
+ issuesubtitle
+ issuetitle
+ issuetitleaddon
+ language
+ note
+ number
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ volume
+ yeardivision
+
+
+ mvproceedings
+ addendum
+ editor
+ editortype
+ eventday
+ eventendday
+ eventendhour
+ eventendminute
+ eventendmonth
+ eventendsecond
+ eventendtimezone
+ eventendyear
+ eventendyeardivision
+ eventhour
+ eventminute
+ eventmonth
+ eventsecond
+ eventtimezone
+ eventyear
+ eventyeardivision
+ eventtitle
+ eventtitleaddon
+ isbn
+ language
+ location
+ note
+ number
+ organization
+ pagetotal
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ venue
+ volumes
+
+
+ proceedings
+ addendum
+ chapter
+ editor
+ editortype
+ eid
+ eventday
+ eventendday
+ eventendhour
+ eventendminute
+ eventendmonth
+ eventendsecond
+ eventendtimezone
+ eventendyear
+ eventendyeardivision
+ eventhour
+ eventminute
+ eventmonth
+ eventsecond
+ eventtimezone
+ eventyear
+ eventyeardivision
+ eventtitle
+ eventtitleaddon
+ isbn
+ language
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ note
+ number
+ organization
+ pages
+ pagetotal
+ part
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ venue
+ volume
+ volumes
+
+
+ inproceedings
+ addendum
+ author
+ booksubtitle
+ booktitle
+ booktitleaddon
+ chapter
+ editor
+ editortype
+ eid
+ eventday
+ eventendday
+ eventendhour
+ eventendminute
+ eventendmonth
+ eventendsecond
+ eventendtimezone
+ eventendyear
+ eventendyeardivision
+ eventhour
+ eventminute
+ eventmonth
+ eventsecond
+ eventtimezone
+ eventyear
+ eventyeardivision
+ eventtitle
+ eventtitleaddon
+ isbn
+ language
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ note
+ number
+ organization
+ pages
+ part
+ publisher
+ pubstate
+ series
+ subtitle
+ title
+ titleaddon
+ venue
+ volume
+ volumes
+
+
+ report
+ addendum
+ author
+ chapter
+ eid
+ institution
+ isrn
+ language
+ location
+ note
+ number
+ pages
+ pagetotal
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+ version
+
+
+ thesis
+ addendum
+ author
+ chapter
+ eid
+ institution
+ language
+ location
+ note
+ pages
+ pagetotal
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+
+
+ unpublished
+ addendum
+ author
+ eventday
+ eventendday
+ eventendhour
+ eventendminute
+ eventendmonth
+ eventendsecond
+ eventendtimezone
+ eventendyear
+ eventendyeardivision
+ eventhour
+ eventminute
+ eventmonth
+ eventsecond
+ eventtimezone
+ eventyear
+ eventyeardivision
+ eventtitle
+ eventtitleaddon
+ howpublished
+ language
+ location
+ note
+ pubstate
+ subtitle
+ title
+ titleaddon
+ type
+ venue
+
+
+ abstract
+ addendum
+ afterword
+ annotator
+ author
+ bookauthor
+ booksubtitle
+ booktitle
+ booktitleaddon
+ chapter
+ commentator
+ editor
+ editora
+ editorb
+ editorc
+ foreword
+ holder
+ institution
+ introduction
+ issuesubtitle
+ issuetitle
+ issuetitleaddon
+ journalsubtitle
+ journaltitle
+ journaltitleaddon
+ location
+ mainsubtitle
+ maintitle
+ maintitleaddon
+ nameaddon
+ note
+ organization
+ origlanguage
+ origlocation
+ origpublisher
+ origtitle
+ part
+ publisher
+ relatedstring
+ series
+ shortauthor
+ shorteditor
+ shorthand
+ shortjournal
+ shortseries
+ shorttitle
+ sortname
+ sortshorthand
+ sorttitle
+ subtitle
+ title
+ titleaddon
+ translator
+ venue
+
+
+ article
+ book
+ inbook
+ bookinbook
+ suppbook
+ booklet
+ collection
+ incollection
+ suppcollection
+ manual
+ misc
+ mvbook
+ mvcollection
+ online
+ patent
+ periodical
+ suppperiodical
+ proceedings
+ inproceedings
+ reference
+ inreference
+ report
+ set
+ thesis
+ unpublished
+
+
+ date
+ year
+
+
+
+
+ set
+
+ entryset
+
+
+
+ article
+
+ author
+ journaltitle
+ title
+
+
+
+ book
+ mvbook
+
+ author
+ title
+
+
+
+ inbook
+ bookinbook
+ suppbook
+
+ author
+ title
+ booktitle
+
+
+
+ booklet
+
+
+ author
+ editor
+
+ title
+
+
+
+ collection
+ reference
+ mvcollection
+ mvreference
+
+ editor
+ title
+
+
+
+ incollection
+ suppcollection
+ inreference
+
+ author
+ editor
+ title
+ booktitle
+
+
+
+ dataset
+
+ title
+
+
+
+ manual
+
+ title
+
+
+
+ misc
+ software
+
+ title
+
+
+
+ online
+
+ title
+
+ url
+ doi
+ eprint
+
+
+
+
+ patent
+
+ author
+ title
+ number
+
+
+
+ periodical
+
+ editor
+ title
+
+
+
+ proceedings
+ mvproceedings
+
+ title
+
+
+
+ inproceedings
+
+ author
+ title
+ booktitle
+
+
+
+ report
+
+ author
+ title
+ type
+ institution
+
+
+
+ thesis
+
+ author
+ title
+ type
+ institution
+
+
+
+ unpublished
+
+ author
+ title
+
+
+
+
+ isbn
+
+
+ issn
+
+
+ ismn
+
+
+ gender
+
+
+
+
+
+
+ Bibliografia.bib
+
+
+ angiuli2022canonicity
+
+
+
+
+ presort
+
+
+ sortkey
+
+
+ sortname
+ author
+ editor
+ translator
+ sorttitle
+ title
+
+
+ sorttitle
+ title
+
+
+ sortyear
+ year
+
+
+ volume
+ 0
+
+
+
+
+
+
diff --git a/Tesi.blg b/Tesi.blg
new file mode 100644
index 0000000..b236029
--- /dev/null
+++ b/Tesi.blg
@@ -0,0 +1,15 @@
+[0] Config.pm:328> INFO - This is Biber 2.21
+[0] Config.pm:331> INFO - Logfile is 'Tesi.blg'
+[31] biber:342> INFO - === Thu May 14, 2026, 14:51:25
+[42] Biber.pm:421> INFO - Reading 'Tesi.bcf'
+[72] Biber.pm:1002> INFO - Found 1 citekeys in bib section 0
+[80] Biber.pm:4487> INFO - Processing section 0
+[84] Biber.pm:4678> INFO - Looking for bibtex file 'Bibliografia.bib' for section 0
+[84] bibtex.pm:1713> INFO - LaTeX decoding ...
+[85] bibtex.pm:1519> INFO - Found BibTeX data source 'Bibliografia.bib'
+[102] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'normalization = NFD' with 'normalization = prenormalized'
+[102] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'variable = shifted' with 'variable = non-ignorable'
+[103] Biber.pm:4307> INFO - Sorting list 'nty/global//global/global/global' of type 'entry' with template 'nty' and locale 'en-US'
+[103] Biber.pm:4313> INFO - No sort tailoring available for locale 'en-US'
+[103] bbl.pm:676> INFO - Writing 'Tesi.bbl' with encoding 'UTF-8'
+[104] bbl.pm:779> INFO - Output to Tesi.bbl
diff --git a/Tesi.log b/Tesi.log
new file mode 100644
index 0000000..1da701b
--- /dev/null
+++ b/Tesi.log
@@ -0,0 +1,884 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.29 (TeX Live 2026/Arch Linux) (preloaded format=pdflatex 2026.4.6) 15 MAY 2026 19:11
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**Tesi.tex
+(./Tesi.tex
+LaTeX2e <2025-11-01>
+L3 programming layer <2026-01-19>
+(/usr/share/texmf-dist/tex/latex/base/book.cls
+Document Class: book 2025/01/22 v1.4n Standard LaTeX document class
+(/usr/share/texmf-dist/tex/latex/base/bk12.clo
+File: bk12.clo 2025/01/22 v1.4n Standard LaTeX file (size option)
+)
+\c@part=\count275
+\c@chapter=\count276
+\c@section=\count277
+\c@subsection=\count278
+\c@subsubsection=\count279
+\c@paragraph=\count280
+\c@subparagraph=\count281
+\c@figure=\count282
+\c@table=\count283
+\abovecaptionskip=\skip49
+\belowcaptionskip=\skip50
+\bibindent=\dimen148
+)
+(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty
+Package: graphicx 2024/12/31 v1.2e Enhanced LaTeX Graphics (DPC,SPQR)
+
+(/usr/share/texmf-dist/tex/latex/graphics/keyval.sty
+Package: keyval 2022/05/29 v1.15 key=value parser (DPC)
+\KV@toks@=\toks17
+)
+(/usr/share/texmf-dist/tex/latex/graphics/graphics.sty
+Package: graphics 2024/08/06 v1.4g Standard LaTeX Graphics (DPC,SPQR)
+
+(/usr/share/texmf-dist/tex/latex/graphics/trig.sty
+Package: trig 2023/12/02 v1.11 sin cos tan (DPC)
+)
+(/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
+File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
+)
+Package graphics Info: Driver file: pdftex.def on input line 106.
+
+(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def
+File: pdftex.def 2025/09/29 v1.2d Graphics/color driver for pdftex
+))
+\Gin@req@height=\dimen149
+\Gin@req@width=\dimen150
+)
+(/usr/share/texmf-dist/tex/latex/amsfonts/amssymb.sty
+Package: amssymb 2013/01/14 v3.01 AMS font symbols
+
+(/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty
+Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
+\@emptytoks=\toks18
+\symAMSa=\mathgroup4
+\symAMSb=\mathgroup5
+LaTeX Font Info: Redeclaring math symbol \hbar on input line 98.
+LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
+(Font) U/euf/m/n --> U/euf/b/n on input line 106.
+))
+(/usr/share/texmf-dist/tex/latex/amscls/amsthm.sty
+Package: amsthm 2020/05/29 v2.20.6
+\thm@style=\toks19
+\thm@bodyfont=\toks20
+\thm@headfont=\toks21
+\thm@notefont=\toks22
+\thm@headpunct=\toks23
+\thm@preskip=\skip51
+\thm@postskip=\skip52
+\thm@headsep=\skip53
+\dth@everypar=\toks24
+)
+(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty
+Package: amsmath 2025/07/09 v2.17z AMS math features
+\@mathmargin=\skip54
+
+For additional information on amsmath, use the `?' option.
+(/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty
+Package: amstext 2024/11/17 v2.01 AMS text
+
+(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty
+File: amsgen.sty 1999/11/30 v2.0 generic functions
+\@emptytoks=\toks25
+\ex@=\dimen151
+))
+(/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty
+Package: amsbsy 1999/11/29 v1.2d Bold Symbols
+\pmbraise@=\dimen152
+)
+(/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty
+Package: amsopn 2022/04/08 v2.04 operator names
+)
+\inf@bad=\count284
+LaTeX Info: Redefining \frac on input line 233.
+\uproot@=\count285
+\leftroot@=\count286
+LaTeX Info: Redefining \overline on input line 398.
+LaTeX Info: Redefining \colon on input line 409.
+\classnum@=\count287
+\DOTSCASE@=\count288
+LaTeX Info: Redefining \ldots on input line 495.
+LaTeX Info: Redefining \dots on input line 498.
+LaTeX Info: Redefining \cdots on input line 619.
+\Mathstrutbox@=\box53
+\strutbox@=\box54
+LaTeX Info: Redefining \big on input line 721.
+LaTeX Info: Redefining \Big on input line 722.
+LaTeX Info: Redefining \bigg on input line 723.
+LaTeX Info: Redefining \Bigg on input line 724.
+\big@size=\dimen153
+LaTeX Font Info: Redeclaring font encoding OML on input line 742.
+LaTeX Font Info: Redeclaring font encoding OMS on input line 743.
+\macc@depth=\count289
+LaTeX Info: Redefining \bmod on input line 904.
+LaTeX Info: Redefining \pmod on input line 909.
+LaTeX Info: Redefining \smash on input line 939.
+LaTeX Info: Redefining \relbar on input line 969.
+LaTeX Info: Redefining \Relbar on input line 970.
+\c@MaxMatrixCols=\count290
+\dotsspace@=\muskip17
+\c@parentequation=\count291
+\dspbrk@lvl=\count292
+\tag@help=\toks26
+\row@=\count293
+\column@=\count294
+\maxfields@=\count295
+\andhelp@=\toks27
+\eqnshift@=\dimen154
+\alignsep@=\dimen155
+\tagshift@=\dimen156
+\tagwidth@=\dimen157
+\totwidth@=\dimen158
+\lineht@=\dimen159
+\@envbody=\toks28
+\multlinegap=\skip55
+\multlinetaggap=\skip56
+\mathdisplay@stack=\toks29
+LaTeX Info: Redefining \[ on input line 2950.
+LaTeX Info: Redefining \] on input line 2951.
+)
+(/usr/share/texmf-dist/tex/latex/amsmath/amsxtra.sty
+Package: amsxtra 1999/11/15 v1.2c AMS extra commands
+LaTeX Info: Redefining \nobreakspace on input line 54.
+)
+(/usr/share/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty
+(/usr/share/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty
+(/usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex
+\pgfutil@everybye=\toks30
+\pgfutil@tempdima=\dimen160
+\pgfutil@tempdimb=\dimen161
+)
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def
+\pgfutil@abb=\box55
+)
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex
+(/usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex)
+Package: pgfrcs 2025-08-29 v3.1.11a (3.1.11a)
+))
+Package: pgf 2025-08-29 v3.1.11a (3.1.11a)
+
+(/usr/share/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty
+(/usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty
+(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex
+Package: pgfsys 2025-08-29 v3.1.11a (3.1.11a)
+
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
+\pgfkeys@pathtoks=\toks31
+\pgfkeys@temptoks=\toks32
+
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.te
+x
+\pgfkeys@tmptoks=\toks33
+))
+\pgf@x=\dimen162
+\pgf@y=\dimen163
+\pgf@xa=\dimen164
+\pgf@ya=\dimen165
+\pgf@xb=\dimen166
+\pgf@yb=\dimen167
+\pgf@xc=\dimen168
+\pgf@yc=\dimen169
+\pgf@xd=\dimen170
+\pgf@yd=\dimen171
+\w@pgf@writea=\write3
+\r@pgf@reada=\read2
+\c@pgf@counta=\count296
+\c@pgf@countb=\count297
+\c@pgf@countc=\count298
+\c@pgf@countd=\count299
+\t@pgf@toka=\toks34
+\t@pgf@tokb=\toks35
+\t@pgf@tokc=\toks36
+\pgf@sys@id@count=\count300
+ (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg
+File: pgf.cfg 2025-08-29 v3.1.11a (3.1.11a)
+)
+Driver file for pgf: pgfsys-pdftex.def
+
+(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def
+File: pgfsys-pdftex.def 2025-08-29 v3.1.11a (3.1.11a)
+
+(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def
+File: pgfsys-common-pdf.def 2025-08-29 v3.1.11a (3.1.11a)
+)))
+(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
+File: pgfsyssoftpath.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfsyssoftpath@smallbuffer@items=\count301
+\pgfsyssoftpath@bigbuffer@items=\count302
+)
+(/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex
+File: pgfsysprotocol.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+))
+(/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty
+Package: xcolor 2024/09/29 v3.02 LaTeX color extensions (UK)
+
+(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg
+File: color.cfg 2016/01/02 v1.6 sample color configuration
+)
+Package xcolor Info: Driver file: pdftex.def on input line 274.
+
+(/usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx)
+Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1349.
+Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1353.
+Package xcolor Info: Model `RGB' extended on input line 1365.
+Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1367.
+Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1368.
+Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1369.
+Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1370.
+Package xcolor Info: Model `Gray' substituted by `gray' on input line 1371.
+Package xcolor Info: Model `wave' substituted by `hsb' on input line 1372.
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex
+Package: pgfcore 2025-08-29 v3.1.11a (3.1.11a)
+
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex
+\pgfmath@dimen=\dimen172
+\pgfmath@count=\count303
+\pgfmath@box=\box56
+\pgfmath@toks=\toks37
+\pgfmath@stack@operand=\toks38
+\pgfmath@stack@operation=\toks39
+)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code
+.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.te
+x) (/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics
+.code.tex) (/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex
+\c@pgfmathroundto@lastzeros=\count304
+))
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfint.code.tex)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex
+File: pgfcorepoints.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@picminx=\dimen173
+\pgf@picmaxx=\dimen174
+\pgf@picminy=\dimen175
+\pgf@picmaxy=\dimen176
+\pgf@pathminx=\dimen177
+\pgf@pathmaxx=\dimen178
+\pgf@pathminy=\dimen179
+\pgf@pathmaxy=\dimen180
+\pgf@xx=\dimen181
+\pgf@xy=\dimen182
+\pgf@yx=\dimen183
+\pgf@yy=\dimen184
+\pgf@zx=\dimen185
+\pgf@zy=\dimen186
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex
+File: pgfcorepathconstruct.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@path@lastx=\dimen187
+\pgf@path@lasty=\dimen188
+) (/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex
+File: pgfcorepathusage.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@shorten@end@additional=\dimen189
+\pgf@shorten@start@additional=\dimen190
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex
+File: pgfcorescopes.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfpic=\box57
+\pgf@hbox=\box58
+\pgf@layerbox@main=\box59
+\pgf@picture@serial@count=\count305
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex
+File: pgfcoregraphicstate.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgflinewidth=\dimen191
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.t
+ex
+File: pgfcoretransformations.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@pt@x=\dimen192
+\pgf@pt@y=\dimen193
+\pgf@pt@temp=\dimen194
+) (/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex
+File: pgfcorequick.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex
+File: pgfcoreobjects.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.te
+x
+File: pgfcorepathprocessing.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+) (/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex
+File: pgfcorearrows.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfarrowsep=\dimen195
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex
+File: pgfcoreshade.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@max=\dimen196
+\pgf@sys@shading@range@num=\count306
+\pgf@shadingcount=\count307
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex
+File: pgfcoreimage.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex
+File: pgfcoreexternal.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfexternal@startupbox=\box60
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex
+File: pgfcorelayers.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex
+File: pgfcoretransparency.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+) (/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex
+File: pgfcorepatterns.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex
+File: pgfcorerdf.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)))
+(/usr/share/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex
+File: pgfmoduleshapes.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfnodeparttextbox=\box61
+)
+(/usr/share/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex
+File: pgfmoduleplot.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty
+Package: pgfcomp-version-0-65 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@nodesepstart=\dimen197
+\pgf@nodesepend=\dimen198
+)
+(/usr/share/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty
+Package: pgfcomp-version-1-18 2025-08-29 v3.1.11a (3.1.11a)
+))
+(/usr/share/texmf-dist/tex/latex/pgf/utilities/pgffor.sty
+(/usr/share/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex))
+(/usr/share/texmf-dist/tex/latex/pgf/math/pgfmath.sty
+(/usr/share/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))
+(/usr/share/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex
+Package: pgffor 2025-08-29 v3.1.11a (3.1.11a)
+\pgffor@iter=\dimen199
+\pgffor@skip=\dimen256
+\pgffor@stack=\toks40
+\pgffor@toks=\toks41
+))
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex
+Package: tikz 2025-08-29 v3.1.11a (3.1.11a)
+
+(/usr/share/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.te
+x
+File: pgflibraryplothandlers.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgf@plot@mark@count=\count308
+\pgfplotmarksize=\dimen257
+)
+\tikz@lastx=\dimen258
+\tikz@lasty=\dimen259
+\tikz@lastxsaved=\dimen260
+\tikz@lastysaved=\dimen261
+\tikz@lastmovetox=\dimen262
+\tikz@lastmovetoy=\dimen263
+\tikzleveldistance=\dimen264
+\tikzsiblingdistance=\dimen265
+\tikz@figbox=\box62
+\tikz@figbox@bg=\box63
+\tikz@tempbox=\box64
+\tikz@tempbox@bg=\box65
+\tikztreelevel=\count309
+\tikznumberofchildren=\count310
+\tikznumberofcurrentchild=\count311
+\tikz@fig@count=\count312
+ (/usr/share/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex
+File: pgfmodulematrix.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfmatrixcurrentrow=\count313
+\pgfmatrixcurrentcolumn=\count314
+\pgf@matrix@numberofcolumns=\count315
+)
+\tikz@expandcount=\count316
+
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+topaths.code.tex
+File: tikzlibrarytopaths.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+))) (/usr/share/texmf-dist/tex/latex/tikz-cd/tikz-cd.sty
+Package: tikz-cd 2021/05/04 v1.0 Commutative diagrams with TikZ
+
+(/usr/share/texmf-dist/tex/generic/tikz-cd/tikzlibrarycd.code.tex
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+matrix.code.tex
+File: tikzlibrarymatrix.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+quotes.code.tex
+File: tikzlibraryquotes.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
+File: pgflibraryarrows.meta.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+\pgfarrowinset=\dimen266
+\pgfarrowlength=\dimen267
+\pgfarrowwidth=\dimen268
+\pgfarrowlinewidth=\dimen269
+))) (/usr/share/texmf-dist/tex/latex/quiver/quiver.sty
+Package: quiver 2025/09/20 quiver
+
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+calc.code.tex
+File: tikzlibrarycalc.code.tex 2025-08-29 v3.1.11a (3.1.11a)
+)
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+decorations.pathmorphing.code.tex
+(/usr/share/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrary
+decorations.code.tex
+(/usr/share/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex
+\pgfdecoratedcompleteddistance=\dimen270
+\pgfdecoratedremainingdistance=\dimen271
+\pgfdecoratedinputsegmentcompleteddistance=\dimen272
+\pgfdecoratedinputsegmentremainingdistance=\dimen273
+\pgf@decorate@distancetomove=\dimen274
+\pgf@decorate@repeatstate=\count317
+\pgfdecorationsegmentamplitude=\dimen275
+\pgfdecorationsegmentlength=\dimen276
+)
+\tikz@lib@dec@box=\box66
+)
+(/usr/share/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorati
+ons.pathmorphing.code.tex))
+(/usr/share/texmf-dist/tex/latex/spath3/tikzlibraryspath3.code.tex
+(/usr/share/texmf-dist/tex/latex/spath3/spath3.sty
+(/usr/share/texmf-dist/tex/latex/l3kernel/expl3.sty
+Package: expl3 2026-01-19 L3 programming layer (loader)
+
+(/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
+File: l3backend-pdftex.def 2025-10-09 L3 backend support: PDF output (pdfTeX)
+\l__color_backend_stack_int=\count318
+))
+Package: spath3 2024/05/31 v2.8 Functions for manipulating PGF soft paths
+
+(/usr/share/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
+Package: xparse 2025-10-09 L3 Experimental document command parser
+)
+\g__spath_output_int=\count319
+\l__spath_tmpa_dim=\dimen277
+\l__spath_tmpb_dim=\dimen278
+\l__spath_tmpa_int=\count320
+\l__spath_tmpb_int=\count321
+\l__spath_move_x_dim=\dimen279
+\l__spath_move_y_dim=\dimen280
+\l__spath_rectx_dim=\dimen281
+\l__spath_recty_dim=\dimen282
+\g__spath_anon_int=\count322
+)
+\l__tikzspath_tmpa_int=\count323
+))
+\c@definition=\count324
+
+(/usr/share/texmf-dist/tex/latex/biblatex/biblatex.sty
+Package: biblatex 2025/07/10 v3.21 programmable bibliographies (PK/MW)
+
+(/usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
+Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO
+)
+
+(/usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty
+Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO)
+)
+(/usr/share/texmf-dist/tex/generic/iftex/iftex.sty
+Package: iftex 2024/12/12 v1.0g TeX engine tests
+)
+(/usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
+Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO)
+)
+Package pdftexcmds Info: \pdf@primitive is available.
+Package pdftexcmds Info: \pdf@ifprimitive is available.
+Package pdftexcmds Info: \pdfdraftmode found.
+)
+(/usr/share/texmf-dist/tex/latex/etoolbox/etoolbox.sty
+Package: etoolbox 2025/10/02 v2.5m e-TeX tools for LaTeX (JAW)
+\etb@tempcnta=\count325
+)
+(/usr/share/texmf-dist/tex/latex/kvoptions/kvoptions.sty
+Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
+
+(/usr/share/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
+Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
+))
+(/usr/share/texmf-dist/tex/latex/logreq/logreq.sty
+Package: logreq 2010/08/04 v1.0 xml request logger
+\lrq@indent=\count326
+
+(/usr/share/texmf-dist/tex/latex/logreq/logreq.def
+File: logreq.def 2010/08/04 v1.0 logreq spec v1.0
+))
+(/usr/share/texmf-dist/tex/latex/base/ifthen.sty
+Package: ifthen 2024/03/16 v1.1e Standard LaTeX ifthen package (DPC)
+)
+(/usr/share/texmf-dist/tex/latex/url/url.sty
+\Urlmuskip=\muskip18
+Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc.
+)
+\c@tabx@nest=\count327
+\c@listtotal=\count328
+\c@listcount=\count329
+\c@liststart=\count330
+\c@liststop=\count331
+\c@citecount=\count332
+\c@citetotal=\count333
+\c@multicitecount=\count334
+\c@multicitetotal=\count335
+\c@instcount=\count336
+\c@maxnames=\count337
+\c@minnames=\count338
+\c@maxitems=\count339
+\c@minitems=\count340
+\c@citecounter=\count341
+\c@maxcitecounter=\count342
+\c@savedcitecounter=\count343
+\c@uniquelist=\count344
+\c@uniquename=\count345
+\c@refsection=\count346
+\c@refsegment=\count347
+\c@maxextratitle=\count348
+\c@maxextratitleyear=\count349
+\c@maxextraname=\count350
+\c@maxextradate=\count351
+\c@maxextraalpha=\count352
+\c@abbrvpenalty=\count353
+\c@highnamepenalty=\count354
+\c@lownamepenalty=\count355
+\c@maxparens=\count356
+\c@parenlevel=\count357
+\blx@tempcnta=\count358
+\blx@tempcntb=\count359
+\blx@tempcntc=\count360
+\c@blx@maxsection=\count361
+\blx@maxsegment@0=\count362
+\blx@notetype=\count363
+\blx@parenlevel@text=\count364
+\blx@parenlevel@foot=\count365
+\blx@sectionciteorder@0=\count366
+\blx@sectionciteorderinternal@0=\count367
+\blx@entrysetcounter=\count368
+\blx@biblioinstance=\count369
+\labelnumberwidth=\skip57
+\labelalphawidth=\skip58
+\biblabelsep=\skip59
+\bibitemsep=\skip60
+\bibnamesep=\skip61
+\bibinitsep=\skip62
+\bibparsep=\skip63
+\bibhang=\skip64
+\blx@bcfin=\read3
+\blx@bcfout=\write4
+\blx@langwohyphens=\language3
+\c@mincomprange=\count370
+\c@maxcomprange=\count371
+\c@mincompwidth=\count372
+Package biblatex Info: Trying to load biblatex default data model...
+Package biblatex Info: ... file 'blx-dm.def' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/blx-dm.def
+File: blx-dm.def 2025/07/10 v3.21 biblatex datamodel (PK/MW)
+)
+Package biblatex Info: Trying to load biblatex custom data model...
+Package biblatex Info: ... file 'biblatex-dm.cfg' not found.
+\c@afterword=\count373
+\c@savedafterword=\count374
+\c@annotator=\count375
+\c@savedannotator=\count376
+\c@author=\count377
+\c@savedauthor=\count378
+\c@bookauthor=\count379
+\c@savedbookauthor=\count380
+\c@commentator=\count381
+\c@savedcommentator=\count382
+\c@editor=\count383
+\c@savededitor=\count384
+\c@editora=\count385
+\c@savededitora=\count386
+\c@editorb=\count387
+\c@savededitorb=\count388
+\c@editorc=\count389
+\c@savededitorc=\count390
+\c@foreword=\count391
+\c@savedforeword=\count392
+\c@holder=\count393
+\c@savedholder=\count394
+\c@introduction=\count395
+\c@savedintroduction=\count396
+\c@namea=\count397
+\c@savednamea=\count398
+\c@nameb=\count399
+\c@savednameb=\count400
+\c@namec=\count401
+\c@savednamec=\count402
+\c@translator=\count403
+\c@savedtranslator=\count404
+\c@shortauthor=\count405
+\c@savedshortauthor=\count406
+\c@shorteditor=\count407
+\c@savedshorteditor=\count408
+\c@labelname=\count409
+\c@savedlabelname=\count410
+\c@institution=\count411
+\c@savedinstitution=\count412
+\c@lista=\count413
+\c@savedlista=\count414
+\c@listb=\count415
+\c@savedlistb=\count416
+\c@listc=\count417
+\c@savedlistc=\count418
+\c@listd=\count419
+\c@savedlistd=\count420
+\c@liste=\count421
+\c@savedliste=\count422
+\c@listf=\count423
+\c@savedlistf=\count424
+\c@location=\count425
+\c@savedlocation=\count426
+\c@organization=\count427
+\c@savedorganization=\count428
+\c@origlocation=\count429
+\c@savedoriglocation=\count430
+\c@origpublisher=\count431
+\c@savedorigpublisher=\count432
+\c@publisher=\count433
+\c@savedpublisher=\count434
+\c@language=\count435
+\c@savedlanguage=\count436
+\c@origlanguage=\count437
+\c@savedoriglanguage=\count438
+\c@pageref=\count439
+\c@savedpageref=\count440
+\shorthandwidth=\skip65
+\shortjournalwidth=\skip66
+\shortserieswidth=\skip67
+\shorttitlewidth=\skip68
+\shortauthorwidth=\skip69
+\shorteditorwidth=\skip70
+\locallabelnumberwidth=\skip71
+\locallabelalphawidth=\skip72
+\localshorthandwidth=\skip73
+\localshortjournalwidth=\skip74
+\localshortserieswidth=\skip75
+\localshorttitlewidth=\skip76
+\localshortauthorwidth=\skip77
+\localshorteditorwidth=\skip78
+Package biblatex Info: Trying to load compatibility code...
+Package biblatex Info: ... file 'blx-compat.def' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/blx-compat.def
+File: blx-compat.def 2025/07/10 v3.21 biblatex compatibility (PK/MW)
+)
+Package biblatex Info: Trying to load generic definitions...
+Package biblatex Info: ... file 'biblatex.def' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/biblatex.def
+File: biblatex.def 2025/07/10 v3.21 biblatex compatibility (PK/MW)
+\c@textcitecount=\count441
+\c@textcitetotal=\count442
+\c@textcitemaxnames=\count443
+\c@biburlbigbreakpenalty=\count444
+\c@biburlbreakpenalty=\count445
+\c@biburlnumpenalty=\count446
+\c@biburlucpenalty=\count447
+\c@biburllcpenalty=\count448
+\biburlbigskip=\muskip19
+\biburlnumskip=\muskip20
+\biburlucskip=\muskip21
+\biburllcskip=\muskip22
+\c@smartand=\count449
+)
+Package biblatex Info: Trying to load bibliography style 'numeric'...
+Package biblatex Info: ... file 'numeric.bbx' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx
+File: numeric.bbx 2025/07/10 v3.21 biblatex bibliography style (PK/MW)
+Package biblatex Info: Trying to load bibliography style 'standard'...
+Package biblatex Info: ... file 'standard.bbx' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
+File: standard.bbx 2025/07/10 v3.21 biblatex bibliography style (PK/MW)
+\c@bbx:relatedcount=\count450
+\c@bbx:relatedtotal=\count451
+))
+Package biblatex Info: Trying to load citation style 'numeric'...
+Package biblatex Info: ... file 'numeric.cbx' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx
+File: numeric.cbx 2025/07/10 v3.21 biblatex citation style (PK/MW)
+Package biblatex Info: Redefining '\cite'.
+Package biblatex Info: Redefining '\parencite'.
+Package biblatex Info: Redefining '\footcite'.
+Package biblatex Info: Redefining '\footcitetext'.
+Package biblatex Info: Redefining '\smartcite'.
+Package biblatex Info: Redefining '\supercite'.
+Package biblatex Info: Redefining '\textcite'.
+Package biblatex Info: Redefining '\textcites'.
+Package biblatex Info: Redefining '\cites'.
+Package biblatex Info: Redefining '\parencites'.
+Package biblatex Info: Redefining '\smartcites'.
+)
+Package biblatex Info: Trying to load configuration file...
+Package biblatex Info: ... file 'biblatex.cfg' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/biblatex.cfg
+File: biblatex.cfg
+)
+Package biblatex Info: Input encoding 'utf8' detected.
+Package biblatex Info: Document encoding is UTF8 ....
+Package biblatex Info: ... and expl3
+(biblatex) 2026-01-19 L3 programming layer (loader)
+(biblatex) is new enough (at least 2020/04/06),
+(biblatex) setting 'casechanger=expl3'.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty
+Package: blx-case-expl3 2025/07/10 v3.21 expl3 case changing code for biblatex
+))
+\@quotelevel=\count452
+\@quotereset=\count453
+
+
+LaTeX Warning: Unused global option(s):
+ [italian].
+
+(./Tesi.aux)
+\openout1 = `Tesi.aux'.
+
+LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 34.
+LaTeX Font Info: ... okay on input line 34.
+ (/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count454
+\scratchdimen=\dimen283
+\scratchbox=\box67
+\nofMPsegments=\count455
+\nofMParguments=\count456
+\everyMPshowfont=\toks42
+\MPscratchCnt=\count457
+\MPscratchDim=\dimen284
+\MPnumerator=\count458
+\makeMPintoPDFobject=\count459
+\everyMPtoPDFconversion=\toks43
+) (/usr/share/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
+Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
+Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
+85.
+
+(/usr/share/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
+File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv
+e
+))
+Package biblatex Info: Trying to load language 'english'...
+Package biblatex Info: ... file 'english.lbx' found.
+
+(/usr/share/texmf-dist/tex/latex/biblatex/lbx/english.lbx
+File: english.lbx 2025/07/10 v3.21 biblatex localization (PK/MW)
+)
+Package biblatex Info: Input encoding 'utf8' detected.
+Package biblatex Info: Automatic encoding selection.
+(biblatex) Assuming data encoding 'utf8'.
+\openout4 = `Tesi.bcf'.
+
+Package biblatex Info: Trying to load bibliographic data...
+Package biblatex Info: ... file 'Tesi.bbl' found.
+ (./Tesi.bbl)
+Package biblatex Info: Reference section=0 on input line 34.
+Package biblatex Info: Reference segment=0 on input line 34.
+LaTeX Font Info: Trying to load font information for U+msa on input line 36.
+
+
+(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd
+File: umsa.fd 2013/01/14 v3.01 AMS symbols A
+)
+LaTeX Font Info: Trying to load font information for U+msb on input line 36.
+
+
+(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd
+File: umsb.fd 2013/01/14 v3.01 AMS symbols B
+) [1
+
+
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2{/usr/share/texmf-dist/f
+onts/enc/dvips/cm-super/cm-super-ts1.enc}] [3]
+Underfull \vbox (badness 1365) has occurred while \output is active []
+
+ [4]
+[5] [6] [7] [8]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [9]
+Overfull \hbox (1.52892pt too wide) in paragraph at lines 396--400
+\OT1/cmr/m/n/12 Now, con-sider the cou-ple $(\OML/cmm/m/it/12 u[]; u[]\OT1/cmr/
+m/n/12 )$; by com-mu-ta-tiv-ity of (11[]) if $(\OML/cmm/m/it/12 u[]; u[]\OT1/cm
+r/m/n/12 ) :
+ []
+
+[10] [11]
+Overfull \hbox (25.67044pt too wide) detected at line 469
+[]
+ []
+
+[12] [13] [14] [15]
+Underfull \vbox (badness 10000) has occurred while \output is active []
+
+ [16]
+[17] [18] [19] [20] [21
+
+] (./Tesi.aux)
+ ***********
+LaTeX2e <2025-11-01>
+L3 programming layer <2026-01-19>
+ ***********
+Package logreq Info: Writing requests to 'Tesi.run.xml'.
+\openout1 = `Tesi.run.xml'.
+
+ )
+Here is how much of TeX's memory you used:
+ 26644 strings out of 469515
+ 568736 string characters out of 5470808
+ 1334979 words of memory out of 5000000
+ 54938 multiletter control sequences out of 15000+600000
+ 640012 words of font info for 86 fonts, out of 8000000 for 9000
+ 14 hyphenation exceptions out of 8191
+ 84i,21n,104p,966b,1242s stack positions out of 10000i,1000n,20000p,200000b,200000s
+<
+/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb>
+Output written on Tesi.pdf (21 pages, 323499 bytes).
+PDF statistics:
+ 192 PDF objects out of 1000 (max. 8388607)
+ 121 compressed objects within 2 object streams
+ 0 named destinations out of 1000 (max. 500000)
+ 13 words of extra memory for PDF output out of 10000 (max. 10000000)
+
diff --git a/Tesi.pdf b/Tesi.pdf
new file mode 100644
index 0000000..0064a95
Binary files /dev/null and b/Tesi.pdf differ
diff --git a/Tesi.run.xml b/Tesi.run.xml
new file mode 100644
index 0000000..7c3a7cc
--- /dev/null
+++ b/Tesi.run.xml
@@ -0,0 +1,85 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+]>
+
+
+ latex
+
+ Tesi.bcf
+
+
+ Tesi.bbl
+
+
+ blx-dm.def
+ blx-compat.def
+ biblatex.def
+ standard.bbx
+ numeric.bbx
+ numeric.cbx
+ biblatex.cfg
+ english.lbx
+
+
+
+ biber
+
+ biber
+ Tesi
+
+
+ Tesi.bcf
+
+
+
+ Tesi.bbl
+
+
+ Tesi.bcf
+
+
+ Bibliografia.bib
+
+
+
diff --git a/Tesi.synctex.gz b/Tesi.synctex.gz
new file mode 100644
index 0000000..aa4c83e
Binary files /dev/null and b/Tesi.synctex.gz differ
diff --git a/Tesi.tex b/Tesi.tex
new file mode 100644
index 0000000..2965f18
--- /dev/null
+++ b/Tesi.tex
@@ -0,0 +1,760 @@
+% !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=WzAsNixbMCwxLCJYIFxcb3BsdXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBIFxcb3BsdXMgQikiXSxbMSwwLCJcXGlvdGFfWCIsMl0sWzIsMCwiXFxpb3RhX1kiXSxbMSwzLCJmIl0sWzIsNCwiZyIsMl0sWzMsNSwiKFxcbWF0aGNhbHtpXzF9KV9cXG1hdGhjYWx7Q30iXSxbNCw1LCIoXFxpb3RhX3syfSlfXFxtYXRoY2Fse0N9IiwyXSxbMCw1LCJcXGV4aXN0cyAhIGYgXFxvcGx1cyBnIl1d¯o_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$ beeing cartesian closed functor is identical to the proof of $\Pi_1$ beeing continous 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. 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}\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 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)$}. \\
+ \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, expliciting 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 unuque $\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)$. Morover, 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{Contrution 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 performe and "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 expliciting 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 succesfully constructed a morhpism $\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 evaulation 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 ismophism 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 objet. 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 catgory
+ \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=¯o_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$
+ \begin{proof}
+ By lemma \ref{cover of cc is cc} $Cov(-)$ exentend 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
+ \[
+ Ff :
+ \]
+ \end{proof}
+ \end{proposition}
+
+
+
+ \printbibliography
+\end{document}
\ No newline at end of file
diff --git a/Tesi.tex.recover.bak~ b/Tesi.tex.recover.bak~
new file mode 100644
index 0000000..ecef88a
--- /dev/null
+++ b/Tesi.tex.recover.bak~
@@ -0,0 +1,653 @@
+% !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}
\ No newline at end of file