\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Cubical Sets}
\subsection{Category of Cubes}
%TODO auto correct
%TODO proof read
%TODO Dedekind cubes
%TODO connections

The first question we need to answer, what site to consider. In the simplicial world there is more
or less a consesus, what exactly the site should be. In the cubical world there are multiple models
with slightly different sites. Our main protagonist will be the cartesian model, but we will also
need to introduce the Dedekind model, as it will appear in an argument later. For a comperative
analysis we direct the reader to \cite{cavalloUnifyingCubicalModels2016} and \cite{ABCHFL}.

\subsubsection{Cartesian cubes}

The most uniform description is probably in form of Lawvere theories,
but our site has a more direct description \cite{mathematicalsciencesresearchinstitutemsriEquivariantUniformKan2020}.

\begin{definition}
	Let \(\mathrm{FinSet}\) be the category whose objects are the subsets of \(ℕ\), of the form \(\{0,..,n\}\), for some
	\(n ∈ ℕ\), and as morphisms functions between them.
\end{definition}

\begin{remark}
	Up to equivalence this is the category of finite sets. Choosing a skeleton will circumvent later size issues, but
	for convenience we will pretend that these are finite sets and not always reindex our sets to have an initial segment
	of \(ℕ\).
\end{remark}

\begin{definition}\label{def:cartCubeSet}
	Let \( □ ≔ {\mathrm{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}^\mathsf{op}\)
	the opposite category of double-pointed finite sets.
\end{definition}

An alternative definition would be
\begin{definition}\label{def:cartCubeTheory}
	Let \(□\) be the Lawvere-theory of the type theory with a single type \I, and
	two constants \(⊥ : \I\) and \(⊤ : \I\).
\end{definition}

\begin{remark}
	As in light of \fref{def:cartCubeSet} and \fref{def:cartCubeTheory} we sometimes talk about morphisms
	as functions \(X + 2 → Y + 2\) preserving both points in \(2\) or equivalently ordinary functions \(X → Y+2\).
\end{remark}

We will now spend some time exploring, why this might be viewed as the cube category.
We write \(\{⊥|a,b,c|⊤\}\) for double pointed finite sets, where \(⊥\) and \(⊤\) are the
two distunguished points. A cube of dimension \(n\) is now interpreted as such a set
with \(n+2\) (\(n\) without the distinguished points) many elements. We think of these
as dimension variables. We could for example think about the zero dimensional cube
(a point) \(\{⊥|⊤\}\) and the 2 dimensional cube (a square) \(\{⊥|a,b|⊤\}\).
How many maps do we expect from the line, into the point? Exactly one. And this is
also exactly what we get, a fitting map in \( \FinSetOp \) corresponds to a function 
\(\{⊥|⊤\} → \{⊥|a,b|⊤\}\) preserving \(⊥\) and \(⊤\), this is already unique.
In the other direction we have four maps. These encode the corners. For example the corner  “\((⊥,⊥)\)”
gets encode by sending \(a\) and \(b\) to \(⊥\).

Lets increase the dimensions a bit and look at the maps from a 1 dimensional cube (a line segment)
\(\{⊥|x|⊤\}\}\) into the square. These correspond to functions from \(\{a,b\} → \{⊥,x,⊤\}\). We
can think of this as a dimensional description of a line in a square. We have 2 dimensions in which
the line can move \(a\) and \(b\). And in this two dimennsions the line can either be constant (sending
this dimension to \(⊥\) or \(⊤\), or can advance along its dimension (sending the dimension to \(x\)).
So we get the degenerate corner points (as lines), by sending both of \(a\) and \(b\) to \(⊥\) or \(⊤\).
We get the for sides of the square by sending one of \(a\) or \(b\) to \(⊥\) or \(⊤\). The two sides
that run along the dimension \(a\) send \(a\) to \(x\).
One function is left, sending both \(a\) and \(b\) to \(x\). This is the line that advances in both
dimensions. Or in other words the diagonal.

\begin{remark}
	Our cube category is closed under taking products. This differs from the simplicial case. This will turn out to be very handy and
	important later.
\end{remark}

As we will need some of these element througout the document again we will give them names.
\begin{definition}[Notation for cubes]\label{def:cubeNotation}
	We call:
	\begin{itemize}
		\item \([0] ≔ \{⊥|⊤\}\)
		\item \([1] ≔ \{⊥|x|⊤\}\)
		\item \(\deg(x) ≔ |x| - 2\)
		\item \(\mathrm{d}_k ­­: [0] → [1]\) with \(k ∈ \{⊤,⊥\}\), be the map given by the function that sends \(x \mapsto k\)
	\end{itemize}
\end{definition}

\begin{figure}
	\centering
	\includesvg[inkscapearea=nocrop,inkscapedpi=500]{figures/square_example_picture.svg}
	\caption{A square with some lines maped into it}
	\todo[inline]{fix 0 to \(⊥\) and same for 1}
\end{figure}


Also while \(□\) is not a strict Reedy-category (as \(Δ\) is) it is almost, namely an Eilenberg-Zilber category.
So most of Reedy theory from the simplicial case can be salvaged. This will play an integral part in the
prove that our model structure on \□ is equivalent to spaces.

\begin{definition}[generalized Reedy-category] %TODO add cite nlab
	A \emph{generalized Reedy category} is a category \C together with two
	wide subcategories \(\C_+\) and \(\C_-\) and a function \(d:\mathrm{ob}(\C) → α\) called \emph{degree},
	for some ordinal \(α\), such that
	\begin{enumerate}
		\item every non-isomorphism in \(\C_+\) raises degree,
		\item every non-isomorphism in \(\C_-\) lowers degree,
		\item every isomorphism in \C preserves degree,
		\item \(\C_+ ∩ \C_-\) is the core of \C
		\item every morphism factors as a mapn in \(\C_-\) followed by a map in \(\C_+\), uniquely up
		to isomorphism
		\item if \(f ∈ \C_-\) and \(θ\) is an isomorphism such that \(θf = f\), then \(θ = \id\)
	\end{enumerate}
\end{definition}

Which will be an important concept later, but in our special case we can do even better

\begin{definition}[Eilenberg-Zilber category] %TODO add cite nlab
	An \emph{Eilenberg-Zilber category} or short \emph{EZ-category} is a small category \C
	equipped with a function \(d:\mathrm{ob}(\C)→ℕ\) such that
	\begin{enumerate}
		\item For \(f : x → y\) a morphism of \C: \label{EZ:1}
		\begin{enumerate}
			\item If \(f\) is an isomorphism, then \(d(x) = d(y)\).
			\item If \(f\) is a noninvertible monomorphism, then \(d(x) < d(y)\).
			\item If \(f\) is a noninvertible split epimorphism, then \(d(x) > d(y)\).
		\end{enumerate}
		\item Every morphism factors as a split epimorphism followed by a monomorphism. \label{EZ:2}
		\item Every pair of split epimorphisms in \C has an absolute pushout. \label{EZ:3}
	\end{enumerate}
\end{definition}

\begin{remark}
	Cleary every EZ-category is a generalized Reedy category
\end{remark}


\begin{theorem}\label{thm:CisEZ}
	\(□\) together with \(\deg\) is an EZ-category
\end{theorem}

Before we give a proof we will give a technical lemma about absolute pushouts of split epis.
\begin{lemma}\label{absolutePushout} %TODO cite nlab absolute pushout
	Let
	\begin{equation*}
		\begin{tikzcd}
			A \arrow[r, two heads, "b"'] \arrow[d, two heads, "c"] & B \arrow[l,bend right, dashed, "b'"'] \arrow[d, two heads, "d_1"'] \\
			C \arrow[r, "d_2"] \arrow[u,bend left, dashed,"c'"] & D \arrow[u, bend right, dashed,"d_1'"']
		\end{tikzcd}
	\end{equation*}
	be a diagram in a category \C of split epis such that, \(bc' = d_1'd_2\). Then it is already a pushout square.
\end{lemma}
\begin{proof}
	We look at an arbitrary cocone
	\begin{equation*}
		\begin{tikzcd}
			A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
			C \arrow[r, "e_2"] & E
		\end{tikzcd}
	\end{equation*}
	We can compose this square with \((c',d_1')\) yielding
	\begin{equation*}
		\begin{tikzcd}
			C \arrow[d,"c'"] \arrow[r, "d_2"] \arrow[dd,bend right, "\id"'] & D \arrow[d,"d_1'"] \\
			A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
			C \arrow[r, "e_2"] & E
		\end{tikzcd}
	\end{equation*}
	We get our candidate map from \(e_1d_1' : D → E\). We need to show that it commuts with \(e_1\) and \(d_1\) as well as
	\(e_2\) and \(d_2\). The second case \(e_1d_1'd_2 = e_2\) is directly obvious from the diagram.
	To check that \(e_1d_1'd_1 = e_1\) it is enough to check that \(be_1d_1'd_1 = be_1\), as \(b\) is epic. Which is a
	straight forward diagramm chase, if one adds all the undrawn arrwos to the diagram above. Since \(d_1\), are epic \(e_1d'_1\) is unique in fulfilling already one of the two conditions.
\end{proof}

\begin{remark}
	As we see in the proof, we don't need \(b\) to be split, but our application needs the split, as split epis are
	preserved by pushouts and general epis are not.
\end{remark}
\begin{remark}
	As split epis and commutativity is preserved by all functors, pushouts of this form are absolute pushouts.
\end{remark}

As we will use the following statement multiple times in the proof we put it into its own lemma.
\begin{lemma} \label{EZ:split}
	Every epi in \(□\) splits. Or dually every mono in \(\FinSet\) has a retraction.
	This can be constructed in a way that for a mono \(f\) in \(\FinSet\) the corresponding contraction
	sends everything not in the image of \(f\) to \(⊥\).
\end{lemma}
\begin{proof}
	Let \(f\) be an epi in \(□\). It is thus a monomorphism in \(\FinSet\). We construct a retraction
	\(g\) (that will be a split in \(□\)). Let  \(g(x)\) by the unique pre image of \(f\) if it is not empty. If it is empty we choose
	any element (for example \(⊥\)). It is trivial to verify that this is a retraction. And as \(f\) needs to
	preserve the destinguished points, \(g\) does to.
\end{proof}

\begin{proof}[Proof of theorem \ref{thm:CisEZ}]
	Property \ref{EZ:1} follows from basic facts about surjectivity and injectivity between finite sets.
	Property \ref{EZ:2} needs us to find a (epi,mono) factorization in \(\FinSet\). This factorization
	can be obtained in the same way one would obtain it \(\Set\), by factoring an morphism through its image.
	It is straight forward to verify, that the distinguished points are preserved by those maps. And the
	that the epi (in \(□\)) splits follows from \ref{EZ:split}.
	
	For property \ref{EZ:3}, we only need find a pushout and splits of the form described in \ref{absolutePushout}.
	So let \(c : A → C\) and \(b : A → B\) spilt epis. We will do this by
	constructing the dual digram in \(\FinSet\). We will keep the names for the morphisms. As pullbacks over non-empty diagrams
	work in \(\FinSet\) like in \(\Set\) we can construct a pullback. Now we must construct the
	dotted arrows that satisfy the dual properties of lemma \ref{absolutePushout}.

	\begin{equation*}
		\begin{tikzcd}
			D \arrow[r, tail ,"b^*c"] \arrow[d,tail, "c^*b"] \pb & B \arrow[d,tail, "b"'] \\
			C \arrow[r,tail,"c"] \arrow[u,dashed, two heads, "(c^*b)'", bend left] & A \arrow[l, bend left,dashed, two heads, "c'"] \arrow[u,bend right,dashed,two heads ,"b'"']
		\end{tikzcd}
	\end{equation*}
	Let \(c'\), \(b'\) and \((c\*b)'\) be retractions of \(c\), \(b\) and \(c^*b\) that sends everything that is not in
	their image to \(0\).
	We will show the required commutativity by case distinction
	Let \(x ∈ C\). Note that \(x ∈ \im c^*b\) if and only if \(c(x) ∈ \im b\) as this is a pullback diagram. Thus it is
	immediatly clear that if \(x\) is not contained in \(\im c^*b\) that  \((b^*c)(c^*b)'(x) = 0 = b'c(x)\). Let us turn to
	the case that \(x ∈ \im c^*b \). As restricted to those \(x\) the map \(c^*b\) is surjective it suffices to check
	\( b'c(c^*b) = (b^*c)(c^*b)'(c^*b) \).
	\begin{equation*}
		(b^*c) = b'b(b^*c) = b'c(c^*b) = (b^*c)(c^*b)'(c^*b) = (b^*c)
	\end{equation*}


 	Thus the corresponding diagram in  \(□\) fulfills the requirements of lemma \ref{absolutePushout}, and is thus
 	an absolute pushout square.
\end{proof}

Next we start looking at the presheaf topos on our cube category \(\hat{□}\).
We will recall some important concepts, and give some construtcion, that we will
use later. Also we introduce some notation.

\begin{definition}[Notation for Cubical Sets]\label{def:notationCubeSets}
	We fix the following notations for Cartesian cubical sets:
	\begin{itemize}
		\item \(* ≔ \Yo{[0]}\)
		\item \(\I ≔ \Yo{[1]}\)
		\item \(δ_k ­≔ \Yo \mathrm{d}_k\)
	\end{itemize}
\end{definition}


\subsubsection{Dedekind cubes}
We will also encounter the so called Dedekind cubes. There are also multiple ways to look at them. We will present
multiple definitions, but skip the equivalence proofs as they don't bear much inside into the subject.

\begin{definition}\leavevmode
	\begin{itemize}
		\item Let \FL be the category of finite lattices and monotone maps.
		\item Let \(𝟚\) be the finite lattice \(⊥ ≤ ⊤\).
	\end{itemize}
\end{definition}

\begin{definition}\label{def:dedCubeLat}
	The category \(□_{∧∨}\) is the full subcategory of \FL, restricted to objects of the form \(𝟚^n\) with \(n ∈ ℕ\).
\end{definition}

\begin{definition}\label{def:dedCubeTheory}
	The category \(□_{∧∨}\) is the Lawvere-theory of the theory of lattices.
\end{definition}

Unraveling this definition gives us a quite similar description to our description of Cartesian cubes.
Let \(F\) be the functor that assigns to a set its free lattice. We have then as objects
natural numbers (or up to equivalence finite sets). And again we will write elements of these as lower
roman letters instead of natural numbers to keep the confusion between sets and their elements minimal.
A morphism \(m → n\) is a function
from \(n → F(m)\). This adds a few more degeneracy maps, but the general geometric intuition stays the
same. The elments of of an object are dimensions, and maps do give us for every dimension in the target
a term, that describes the behaiviour of our domain in that particular direction. If we look at an
example again one might ask what the difference is, between the new degeneracies map from a square
to the interval in comparison to the old one. We can view these as degenrate squares where we map the top
and right (or bottom and left) side along the interval and the other to sides to \(⊥\) (or \(⊤\)).
This wasn't possible before and will make a drastic difference once we start considiring filling and
composition problems.

\begin{figure}
\missingfigure{draw pictures for this}
\caption{A squre degenrated with a connection. The upper and right side are equal while the left and bottom side is degenrated to point.}
\end{figure}

\todo{add figure for \(2→2\) degeneracy map}

\begin{proposition}
	The Dedekind cubes are an EZ-category
\end{proposition}
\begin{proof}[Proof sketch:]
	This can be proven by an analog argument as \fref{thm:CisEZ}
\end{proof}

If it is clear from the context we will use the notation from \fref{def:cubeNotation} and \fref{def:notationCubeSets} for
the anologous objects of the Dedekind cubes.

\todo{think about if I want to write down the proof}


% We want to recall universes though, as they will become important later again.
% As a warm-up lets consider \(\Set\), as the presheaves over the singleton category.
% We now want to classify all small sets indexed by some set. This is relatively easy, we take the set
% of all small sets, lets call it \(U\) and the set of all elements of all small sets \(E ≔ ∐_{u ∈ U} u\)
% together with the map \(p_U : E → U\) sending each element back to the set where it came from
% \(p_U(s,x) ≔ s\). Another way to express \(E\) would be in term of pointed samll sets, so could
% equivalently define \(E ≔ \Set_{κ}^{*}\). So how do we recover a collection of small sets from this? We just take
% from our potential index set \(α : X → U\) to U. We can then get a pullback.
% \begin{equation}
% \begin{tikzcd}
% 	A \arrow[d,"α^{*}p_u"] \arrow[r] \arrow[dr,phantom, "\lrcorner", very near start] & E \arrow[d,"p_U"] \\
% 	X \arrow[r,"α"] & U
% \end{tikzcd}
% \end{equation}
% And get small sets indexed by \(X\) by sending \(x \mapsto α^{*}p_u^{-1}(x)\). But can we get all those maps
% as pullbacks? Indeed we can, given such a map \(p\) we define \(α(x) ≔ p^{-1}(x)\). Or in more categorical
% terms we are \(α\) sends \(x\) to the collection of \(a\) such that the following diagram commutes.
% \begin{equation}
% 	\begin{tikzcd}
% 		\Yo{*} \arrow[r,"a", dashed] \arrow[d,"\id"] & A \arrow[d,"p"] \\
% 		\Yo{*} \arrow[r,"x"] & X
% 	\end{tikzcd}
% \end{equation}
% 
% Now let us get back to an arbitrary presheaf category. Let \(\C\) be a category, that we will use as
% our site from here on.
% We first need to make percise what our analogon for
% small set, and collection for small indexed sets is.
% 
% \begin{definition} %TODO cite to awodeyKripkeJoyalForcingType2021 Definition 1.1 ? % TODO fix newline shit
% 	\begin{enumerate}
% 		\item A presheaf is called small if all its values are small
% 		\item A map of presheaves \(p : A → X \) is small if for every \(x : \Yo c → X \) the
% 		  presheaf \(A_x\) obtained by the pullback
% 		  \begin{equation*}
% 		  \begin{tikzcd}
% 			  A_x \arrow[r] \arrow[d] \arrow[dr, phantom, "\lrcorner", very near start]  & A \arrow[d,"p"] \\
% 			  \Yo c \arrow[r,"x"] & X
% 		  \end{tikzcd}
% 			\end{equation*}
% 		  is small.
% 	\end{enumerate}
% \end{definition}
% 
% We want now to mimic the set case, so let us first look at, how \(α\) would look, if we just do
% the straight forward generalization.
% \begin{equation*}
% 	\begin{tikzcd}
% 		\Yo d \arrow[r,dashed, "a"] \arrow[d,"\Yo f"] & A \arrow[d,"p"] \\
% 	  \Yo c \arrow[r,"x"] & X
% 	\end{tikzcd}
% \end{equation*}
% Notice that we gained an additional dependency, that this diagram depends on, namely \(f\).
% This makes \(α(x)\) a (small) presheaf on \(\C / c \). And gives rise to the follwing definition:
% 
% \begin{equation}
% 	U(c) ≔ \Obj [ (\C / c)^{\op},\Set_{κ}]
% \end{equation}
% The action on \(U(f)\) for \(f : d → c \) in \(\C\) is given by precomposition with the induced functor
% \( \C / d → \C / c \). And similiar to the \(\Set\) case we can define:
% \begin{equation}
% 	E(c) ≔ \Obj [ (\C / c)^{\op},\Set^{*}_{κ}]
% \end{equation}
% and let the forgetfull functor \(\Set^{*} → \Set\) induce \(p_U : E → U\).
% 
% 
% There are lots of equivalent descriptions of the suboject classifier \(Ω\), we want to recall one quite similiar to our universe
% definition. We call \(\mathbf{2}\) the category of the well-ordering with two elements \( 0 ≤ 1 \).
% 
% \begin{definition}
% 	We define
% 	\begin{equation*}
% 		Ω(c) ≔ \Obj[(\C / c)^{\op},\mathbf{2}]
% 	\end{equation*}
% 	The natural transformation \(\t: * → Ω\) is given by the presheaves that have constant value 1. We call
% 	\(\t\) a \emph{suboject classifier} ttt
% \end{definition}
\end{document}
