\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Equivalence to spaces}\todo{\printline do I need to explain idempotent completions?}
\todo{give all natural transformations \(⇒\) instead of \(→\)}

For this section we fix the following notation. We write \(n\) for a set with cardinality \(n\),
and identify \(2\) with the set \(\{⊥,⊤\}\). We write \([n]\) for the well ordered sets
\(\{0,…,n\}\).

We would love to compare the model categories on \(\□\) and \(\Δ\). For this we want at least
an adjoint pair between those. If we somehow could get a functor on the site level, we could
get an adjoint triple. But there is no immediate obvious functor to do the job.
The usual trick would be to go look at the idempotent completions of these categories. These
usually have :w
more objects and are sometimes more suitable as the codomain of a functor, while
the presheaf category stays the same (up to equivalence).
For example, the idempotent completion of \dCube is the category \FL of finite lattices and
monotone maps \cites{streicherSimplicialSetsCubical2021}{sattlerIdempotentCompletionCubes2019}.
So we have automatically \(\widehat{\FL} = \dcSet\),
and there is an obvious inclusion \(i: Δ → \FL\). Sadly for us \(□\) is already idempotent complete.
To get around this issue we can embed \(j: □ → \dCube → \FL\), and get into the following situation.

\begin{equation*}
	\begin{tikzcd}[column sep=large]
		\□ \arrow[from=r,"j^*"{description,name=i}] & \widehat{\FL} %
		\arrow[from=l,bend left=50,"j_!"{above,name=ish}] \arrow[from=l,bend right=50, "j_*"{below,name=ist}] %
		\arrow[from=r,bend right=50, "i_!"{above,name=jsh}] \arrow[from=r,bend left=50,"i_*"{below,name=jst}] %
		& \Δ \arrow[from=l,"i^*"{description,name=j}]
		\arrow[phantom,from=i,to=ish,"{\rotatebox{270}{\(⊣\)}}"]
		\arrow[phantom,from=ist,to=i,"{\rotatebox{270}{\(⊣\)}}"]
		\arrow[phantom,from=j,to=jsh,"{\rotatebox{270}{\(⊣\)}}"]
		\arrow[phantom,from=jst,to=j,"{\rotatebox{270}{\(⊣\)}}"]
	\end{tikzcd}
\end{equation*}

We can also define \(j\) explicitly like this:
\begin{definition}
	Let \(𝟚\) be the finite order \(⊥ ≤ ⊤\). If it is convenient we will identify this with the order \(0 ≤ 1\). 
\end{definition} \todo{\printline move this somewhere sane}

\begin{definition}\label{def:j}
  Let \(j : □ → \FL\) the functor given by the following data:
  \begin{itemize}
	  \item On objects: \(f(\{⊥|x_1…x_n|⊤\}) ­≔ 𝟚^n\) \todo{\printline use \(⊥⊤\) notation in introduction chapter}
	  \item On morphisms: \(j(f)(g)(x) ≔ \begin{cases}g(f(x)) & f(x) \notin 𝟚 \\ f(x) & f(x) ∈ 𝟚\end{cases}\)
  \end{itemize}
\end{definition}

In \cite{riehlVid} it is claimed that \(i^*j_!\) is the triangulation functor and \(j^*i_!\) a
left Quillen homotopy inverse. In the mean time Reid Barton observed in an yet unpublished paper,
\todo{\printline how to cite this? claimed in \cite{solution}}
that this triangulation can be described by a single functor on the level of sites \(Δ → □\). One
could now establish Quillen equivalence using this functor, for details see \cite[sec. 6]{solution}.
We are going to verify the original argument. To give an overview of the necessary steps:
\begin{enumerate}
	\item Show that \(i_!\) and \(i^*\) are left Quillen. \label{step1}
	\item Show that \(j_!\) and \(j^*\) are left Quillen. \label{step2}
	\item[*] Conclude that all 4  preserve weak equivalences.
  \item Show that \(i_! j^*\) and \(j_! i^*\) descend to inverses of the Homotopy Categories.
\end{enumerate}

Before we jump into the formal proofs we like to get some intuition for the four functors of interest.
The category \FL has the luxury as containing
both \(Δ\) as the well orderings and \dCube as \(𝟚^n\). As \FL is the idempotent completion of \dCube,
we also know that a presheaf on \FL is completely determined by its behavior on \dCube. The two functors
\(i^*\) and \(j^*\) are just the restrictions, and we can also understand \(i_!\) and \(j_!\) geometrically.
Let \(F ∈ \Δ\), then \(F(x) = i_!(F)(i(x))\). The interesting question is what does \(i_!\) define
on cubes (aka \(\Yo 𝟚^n\)) and \(j_!\) on simplicials (aka \(\Yo [n]\)). \(j_!\) will basically triangulate the cube (see \cref{prop:triangulation}),
while \(i_!\) will add just all possible cubes that are degenerated to simplicials.

To understand \(i^*\) a bit better we might take a look how things that are defined on \(𝟚^n\) extend to simplicials.
For this we need to exhibit \([n]\) as a retract of \(𝟚^n\). For this we define two maps.
\begin{definition}
	Let
	\begin{itemize}
		\item \(r: 𝟚^n → [n]\) be the monotone function \(r(f) = Σ_{x ∈ n}f(x)\)
		\item \(i: [n] → 𝟚^n\) be the monotone function \(i(x)(y) = \begin{cases} ⊤ & y < x \\ ⊥ & \text{otherwise} \end{cases}\)
	\end{itemize}
\end{definition}
We can see directly that this is a split retract pair and thus gives rise to an idempotent \(e = ir : 𝟚^n → 𝟚^n\).
And by general abstract nonsense we get that \(r\) is an absolute coequalizer map of \(e\) and \(\id\). Similarly \(i\)
is an absolute equalizer of \(e\) and \(\id\). So for a presheaf
\(F\) on \FL, we can compute \(F([n])\) as the equalizer of \(F(e)\) and \(F(\id)\), or the coequalizer of \(F(e)\) and \(F(\id)\)
in \Set.

\begin{proposition}\label{prop:i_!Nothing}
	\(i_!Δ^n\) agrees with \(\Yo [n]\).
\end{proposition}
\begin{proof} We have
	\begin{equation*}
		\Hom_{\FL}(i_!Δ^n,B) = \Hom_{\Δ}(Δ^n,i^*B) = B(i([n])) = B([n]) = \Hom_{\FL}(\Yo [n], B) \text{,}
	\end{equation*}
	and by uniqueness of adjoints, the claim follows.
\end{proof}

\begin{proposition}\label{prop:j_!Nothing}
	\(j_!(\I^n) = \Yo 𝟚^n\)
\end{proposition} \todo{\printline move to a sane place}
\begin{proof}
	We have that \(\Hom(j_!(\I^n),B) = \Hom(\I^n,j^*(B))\). And we get
	\begin{equation*}
		\Hom(\Yo 𝟚^n, B) = B(𝟚^n) = B(j(n)) = \Hom(\I^n,j^*B)\text{.}
	\end{equation*}
	Thus, by uniqueness of adjoints, we have that \(j_!(\I^n) = \Yo 𝟚^n\).
\end{proof}

\subsection{\(i_!\) and \(i^*\) are left Quillen functors}
We need to show that \(i_!\) and \(i^*\) preserve cofibrations (or
in other words monomorphisms) and trivial cofibrations. The hard
part will be to show that \(i_!\) preserves monomorphisms and we will do that last.

\begin{lemma}\label{lem:restrictionPreserveMonos}
Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B} → \hat{\A}\) preserves monomorphisms.
\end{lemma}
\begin{proof}
	Let \(f\) be a monomorphism in \(\hat{\B}\). As being monic can be tested componentwise, we need
	to show that \((i^*f)_x\) is monic for an arbitrary \(x∈\A\). This is just \(f_{(ix)}\) which is monic by assumption.
\end{proof}

\begin{proposition}\label{prop:i*preservesMonos}
	\(i^*\) preserves monomorphisms.
\end{proposition}
\begin{proof}
	Directly by \cref{lem:restrictionPreserveMonos}.
\end{proof}

\begin{proposition}\label{prop:i*preservesTrivialCofib}
	\(i^*\) preserves trivial cofibrations.
\end{proposition}
\begin{proof}
	We are in the comfortable position of being left and right adjoint.
	\(i^*\) preserves the interval inclusion. As pushout products with the interval inclusion sends cofibrations
	to trivial cofibrations and \(i^*\) preserves monomorphisms by \cref{prop:i*preservesMonos}, \(i^*\) sends trivial cofibrations
	to trivial cofibrations.
\end{proof}

As the next proof is mostly a straight forward induction, we don't repeat the full argument and only give a proof sketch.
\begin{proposition}[{\cite[prop. 3.6]{sattlerIdempotentCompletionCubes2019}}]\label{prop:i!preservesTrivialCofib}
	\(i_!\) preserves trivial cofibrations.
\end{proposition} \todo{\printline maybe give the full proof but low prio}
\begin{proof}[Proof sketch.]
	It is fairly easy to see that \(i_!(\Yo -)\) on morphisms is valued in weak equivalences, by checking that representables in \dcSet are
	weakly contractible.
	Then one shows inductively that one can build the horn inclusions as pushouts of horn inclusion of dimension \(n\) and an
	inclusion of the \(n\)-dimensional horn into a \(n+1\) dimensional horn. As \(i_!\) is cocontinuous and the trivial cofibrations
	have as a left lifting class the necessary closure properties, the claim follows.
\end{proof}

We now get to the difficult part of step \ref{step1}. The argument we are going to follow is due to Sattler \cite{sattlerIdempotentCompletionCubes2019}
and involves the Reedy Structure of \(Δ\). We are going through the whole argument here, as it is a good preparation
for \(j_!\) in step \ref{step2}. We also use this to add a lot of detail and improve the criterion a bit, see the remark at \cref{lem:idemLemma3.5}.
\begin{proposition}[{\cite[prop. 3.3]{sattlerIdempotentCompletionCubes2019}}]\label{prop:i!preservesMonos}
	\(i_!\) preserves monomorphisms.
\end{proposition}
Following \cite{sattlerIdempotentCompletionCubes2019} we are first going to prove two technical lemmas.
Note that a repetition of this argument is also good to check if we actually need an elegant Reedy structure
or if we can do with just an Eilenberg-Zilber category.

\begin{lemma}[{\cite[lem 3.4]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.4}
	Let \C be an Eilenberg-Zilber category. Assume \C as pullbacks along face maps.
	The functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
\end{lemma}
\begin{remark}
	The original source has as an extra condition that these pullbacks preserve face and degeneracy maps. We
	do not need this by making use of the fact that degeneracies split.
\end{remark}

For this proof we will make some use of the equivalence between presheaves and discrete Grothendieck fibrations.
This has the benefit of exhibiting our monomorphism as a Grothendieck fibration. We also can lift the
Eilenberg-Zilber structure from our site, a notion that is hard to express with presheaves.

\begin{lemma}\label{lem:liftEZFib}
	Let \(\C\) be an Eilenberg-Zilber category, and \(\p : Q → \C\) a discrete Grothendieck fibration.
	Then we can lift the Eilenberg-Zilber structure to \(Q\).
\end{lemma}
The hard part of the proof will be the lifting of absolute pushouts. In general pushouts don't need to
lift, as the fiber above the pushout in the base category might be empty. If we had a split pushout like in
\cref{absolutePushout}, we could lift the splits to solve that problem. Sadly, not all absolute pushouts
are of this form, but something a bit weaker is true. The first appearance of this observation seems to be
in \cite{pareAbsoluteColimits1971}.
\begin{lemma}\label{lem:absPushChar}
	A commutative square
	\begin{eqcd*}
		A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "m"] \\
		C \arrow[r, "n"] & P
	\end{eqcd*}
	is an absolute pushout diagram if and only if there exists
	\begin{enumerate}
		\item A section \(u : P → B\) of \(m\).
		\item Morphisms \(r_1,…,r_k : B → A \) and \(s_1,…,s_k : B → A\) for some \( k ≥ 1\), such that \(ps_1 = \id_B\),
    \(qs_i = qr_i\) for all \(i\), \(pr_i = ps_{i+1}\) for all \(i < k\), and \(pr_k = um\).
    \item Morphisms \(t_1,…,t_{l+1} : C → A\) and \(v_1,…,v_l : C → A\) for some \(l ≥ 0\), such that \(qt_1 = \id_C\),
    \(pt_i = pv_i\) for all \(i < l\), \(qv_i = qt_{i+1}\) for all \(i ≤ l\), and \(pt_{l+1} = un\).
	\end{enumerate}
	or the symmetric situation where \(B\) and \(C\) are interchanged.
\end{lemma}
\begin{proof}
	Let us assume first we have given all the data above (and WLOG \(B\) and \(C\) are not interchanged), and let
	\begin{eqcd*}
		A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "b"] \\
		C \arrow[r, "c"] & X
	\end{eqcd*}
	be a commutative square. As all this data gets preserved by any functor we only need to prove that such a diagram
	is already a pushout. We now need to find a \(x : P → X\) that witnesses \(P\) as a pushout.
	Since \(m\) splits, \(x\) will be unique automatically. We define \(x ≔ bu\). We now need to check
	if it makes the both evident triangles commute. We do this by chasing though all the data we have been given.
	\begin{equation*}
		xm = bum = bqr_k = cqr_k = cqs_k = bps_k = bqr_{k-1} = … = bps_1 = b
	\end{equation*}
	and
	\begin{equation*}
		xn = bun = bpt_{l+1} = cqt_{l+1} = cqv_l = bpv_l = bpt_l = … = cqt_1 = c \text{.}
	\end{equation*}

  Now let us assume the given square is an absolute pushout. Now we need to construct all the date from above.
  To get the desired split \(u\), we will apply the \(\Hom(P,−)\) functor and get a pushout square in \(\Set\).
  \begin{eqcd*}
	  \Hom(P,A) \arrow[r, "p"] \arrow[d, "q"] \pu & \Hom(P,B) \arrow[d, "m"] \\
		\Hom(P,C) \arrow[r, "n"] & \Hom(P,P)
  \end{eqcd*}
  That means we have a surjection from \(\Hom(P,B) + \Hom(P,C) → \Hom(P,P)\).
  A preimage of \(\id_P\) under this surjection is a morphism \(u\) for that either \(mu = \id_P\)
  or \(nu = \id_P\) holds. We assume WLOG the first case.

  To get \(r_1,…,r_k\) and \(s_1,…,s_k\) that relate \(\id_B\) and \(um\), we look at the image under the
  \(\Hom(B,−)\) functor.
  \begin{eqcd*}
	  \Hom(B,A) \arrow[r, "p"] \arrow[d, "q"] \pu & \Hom(B,B) \arrow[d, "m"] \\
		\Hom(B,C) \arrow[r, "n"] & \Hom(B,P)
  \end{eqcd*}
  We know that \(um\) and \(\id_B\), are getting sent to the same map in \(\hom(B,P)\), because
  \(mum = m = m\id_B\).
  We can now construct a sequence of maps in \(\hom(B,A)\) if we alternate between taking preimages of images
  under \(p\) and \(q\). Lets call the preimages along \(p\) by \(s_i\), and the preimages along \(q\) by \(r_i\).
  This procedure immediately guarantees the equations
  \begin{align*}
	  qs_i = qr_i & & pr_i = ps_{i+1} \text{.}
  \end{align*}
  If we start the procedure with \(\id_B\) in \(\hom(B,B)\), we also get \(ps_1 = \id_B\). Because \(\id_B\) and
  \(um\) get sent to the same element along \(m\) there exists a \(k\) and a choice of \(r_i\) and \(s_i\) such that
  \(pr_k = um\).

  The maps for condition three can be constructed with the same technique after applying the \(\hom(C,−)\) functor.
  The index shift comes from the fact that \(\id_C ∈ \hom(C,C)\) and \(un ∈ \hom(C,B)\) are in opposite corners
  of the resulting diagram.
\end{proof}

To be able to lift this structure, we make sure we can lift commuting triangles first.
\begin{lemma}\label{lem:gfibliftcommute}
	Let \(F : Q → \C\) be a discrete Grothendieck fibration, \(f: A → B\) be a morphism in \(Q\), and
	\(g : C → F(B)\) and \(h : F(A) → C\) such that \(gh = F(f)\). We can lift \(g\) and \(h\) to form
	a commutative diagram in \(Q\).
	\begin{eqcd*}[column sep=small]
		A \arrow[rr,"f"] \arrow[dr, dashed, "h'"'] &    & B \\[-10pt]
		  & C' \arrow[ur,"g'"', dashed]& \\
		F(A) \arrow[rr,"F(f)"] \arrow[dr, "h"'] & & F(B) \\[-10pt]
		 & C \arrow[ur, "g"'] &
	\end{eqcd*}
\end{lemma}
\begin{remark}
	It also suffices to just give an object \(B\) and a commutative diagram in \C.
\end{remark}
\begin{proof}
	That we can get lifts \(g'\) and \(h'\) follows directly from the definition of discrete Grothendieck fibrations.
	We only need to argue that the domain of \(h'\) is indeed \(A\) and that the diagram commutes. As \(f\) and \(g'h'\) are lifts
	of \(F(f) = gh\), we get \(f = g'h'\) by the uniqueness of lifts.
\end{proof}

\begin{proof}[Proof of Lemma \ref{lem:liftEZFib}]
	First we need to define a degree function \(\d : \Obj Q → ℕ\). Let \(\d'\) be the degree function from
	\C, we then define \(\d ≔ \d' \p\). The next thing to do is to show that isomorphisms preserve degree, split epis
	lower degree and noninvertible monomorphisms increase degree. For that it suffices to show that \(p\) preserves
	these. Isomorphisms and split epis are preserved by every functor, so only noninvertible monomorphisms remain.
	We will establish this in two steps, first showing mono preservation and then reflection of inverses.

	Given some monomorphism \(f : A ↣B\) in \(Q\) and two morphisms \(g,h : C → \p(A)\) in \C, such that \(\p(f)h = \p(f)g \),
	we can lift \(g\) and \(h\) to \(g' : C' → A\) and \(h' : C' → A\). By \cref{lem:gfibliftcommute}, we have \(fg' = fh'\) and
	thus \(g' = h'\). We get directly \( g = \p(g') = \p(h') = h\) and thus \(\p(f)\) is monic.

	Assume we have a map \(f\) in \(Q\) such that \(\p(f)\) has a (one sided) inverse. By \cref{lem:gfibliftcommute}, the lift
	of that (one sided) inverse is also a (one sided) inverse of \(f\).

	This fact also helps us directly in the next step. We need to show that every morphism factors into a split epi followed by
	a monomorphism. We can lift a factorization by \cref{lem:gfibliftcommute}, and as one sided inverses are preserved by lifting,
	\(\p\) reflects split epis. So we only need to show that monos are preserved by liftings. Let \(f : A → B\) be a morphism
	in \(Q\), such that \(\p(f)\) is monic and let \(g,h : C → A\) such that \(fg = fh\). Because \(p(f)\) is monic, \(\p(g) = \p(h)\),
	and thus \(g\) and \(h\) are liftings of the same morphism. As liftings are unique \(g = h\) and \(f\) is monic.

	As a last step we must establish that a span of split epis has an absolute pushout. So let \(f: A → B \) and \(g : A → C\) be spilt
	epimorphisms in \(Q\). As these are preserved by functors, \(\p(f)\) and \(\p(g)\) are split epis too. So there is an absolute pushout
	of \(\p(f)\) and \(\p(g)\). By \cref{lem:absPushChar}, we can extend this square, by all the extra morphisms that characterize
	the absolute pushout. We first lift the split established by 1. in \cref{lem:absPushChar}, to get our candidate pushout.
	Lifting the rest of the data and checking that the required equalities still hold is a tedious but straight forward repeated
	application of \cref{lem:liftEZFib}. Afterwards we can apply \cref{lem:absPushChar} again to verify that we indeed got
	an absolute pushout in \(Q\).
\end{proof}
\begin{remark}
	With the exact same argument we can lift elegant Reedy structures. We don't even need to to check the mono preservation,
	we can just define face maps to be lifts of face maps. Even though not explicit in the definition degeneracies in elegant
	reedy categories are split epimorphisms. We took the extra effort here to see if this step would be a problem in the cubical
	case.
\end{remark}

\begin{lemma}\label{lem:liftPullbacks}
	Let \(F : Q → \C\) be a discrete Grothendieck fibration. Given a span in \(Q\) and a pullback of the image of the
	span in \C, then there exists a lift of that pullback completing the original span to a pullback square.
\end{lemma}
\begin{proof}
	Let \(p : A → C\) and \(q : B → C\) be a span in \(Q\), such that its image under \(F\) completes to a pullback
	square. We can lift this square to a commuting square in \(Q\) by \cref{lem:gfibliftcommute}.
	We now need to check that this again a pullback square.
	\begin{eqcd*}[column sep=tiny, row sep=small]
		X \arrow[dd, bend right, "x"' ] \arrow[rrrd, bend left=15, "y"] \arrow[dr, dashed] & & & \\
		  & P' \arrow[rr,"p'"] \arrow[dl,"q'"'] & & A \arrow[dl,"f"] \\
		B \arrow[rr,"g"'] & & C & \\[30pt]
		F(X) \arrow[dd, bend right, "F(x)"'] \arrow[rrrd, bend left=15, "F(y)"] \arrow[dr, dashed] & & & \\
		  & P \arrow[rr,"p"] \arrow[dl,"q"'] \pb & & F(A) \arrow[dl,"F(f)"] \\
		F(B) \arrow[rr, "F(g)"'] & & F(C) &
	\end{eqcd*}
	So let us take any span \((x,y)\) that completes the cospan \((f,g)\) to a commuting square in \(Q\).
	We can map this to \C via \(F\) and get a universal map witnessing that the square in \C is indeed a pullback.
	We can lift this map uniquely to \(P'\) along \(F\), and by lemma \ref{lem:gfibliftcommute} this lift makes the
	diagram commute. 
\end{proof}

% We will also need another technical property of discrete Grothendieck fibrations and Eilenberg-Zilber categories.
% \begin{lemma}\label{lem:bifib}
% 	Let \(F : P ↣ \C\) be a a monic discrete Grothendieck fibration, and \C be an Eilenberg-Zilber (or elegant Reedy) category. Then
% 	\(F\) as opcartesian lifts of degeneracy maps. \todo{\printline check if we introduced “degeneracy” and “face” as words in the definition} 
% \end{lemma}
% \begin{proof}
% 	So let \(A\) be an object in P and \(f : F(A) → B\) be a degeneracy in \C i.e. a split epi.
% 	We can then lift the split to \(A\), and get a morphism \(g : B' → A\) where \(B'\) is the unique object
% 	above \(B\). We can now lift \(f\), to \(B'\) and get a morphism \(f': A → B'\) above \(f\). Verifying that
% 	\(f'\) has the required universal property is a straight forward repeated application of lemma \ref{lem:gfibliftcommute}.
% \end{proof}

\begin{proof}[Proof of Lemma \ref{lem:idemLemma3.4}]
	Let \(f : P' ↣ Q'\) be a monomorphism in \(\hat{\C}\). This gives equivalently rise to a monomorphism \(F\)
	of discrete Grothendieck fibrations via the category of elements.
	We define \(P ­≔ \int P'\), \(Q ≔ \int Q'\) and \(F ≔ \int f\).
	\begin{equation*}
		\begin{tikzcd}[column sep=tiny, row sep=small]
			P \arrow[rr,"F",tail] \arrow[rd] & & Q \arrow[ld] \\
			& \C &
		\end{tikzcd}
	\end{equation*}
	That \(\colim\) sends \(f\) to a monomorphism,
	is equivalent to the statement that \(F\) is monic on connected components. That follows directly from the explicit construction
	of colimits in \(\Set\). Also \(F\) gets to be a discrete Grothendieck fibration on its own. We can lift the Eilenberg-Zilber
	structure to \(Q\) by \cref{lem:liftEZFib}.

	So now let \(S\) and \(T\) be be objects of \(P\) such that \(F(S)\) and \(F(T)\) lie in the same connected component of \(Q\).
	This means there is a zigzag connecting \(F(S)\) and \(F(T)\). We can normalize this to a span. To see this, we are going
	to show how to turn a cospan into a span of morphisms. So let \( f : D → B\) and \( g : E → B \) be a cospan. Because of the Eilenberg-Zilber
	structure, we can factor those into a degeneracy followed by a face map. Lets call them \(f_d\), \(f_f\), \(g_d\) and \(g_f\).
	\begin{eqcd*}[column sep=small]
		D  \arrow[dr, two heads, "f_d"] &   & P \arrow [dr, tail] \arrow[dl, tail] \arrow[dd, phantom,very near start, "\rotatebox{-45}{\(\lrcorner\)}"]&   & E \arrow[dl, two heads, "g_d"'] \\
		{} & • \arrow[dr, tail, "f_f"] \arrow[lu, bend left] &   & • \arrow[dl,tail, "g_f"'] \arrow[ru, bend right] & \\
		{} &  & B &   &  
	\end{eqcd*}
	We can then construct the pullback \(P\) along \(f_f\) and \(g_f\), and the resulting maps concatenated with the splits of \(f_d\) and \(g_d\)
	are a span over \(D\) and \(E\). This means \(F(S)\) and \(F(T)\) are connected by a span of morphisms. Because \(F\) is injective
	on objects we can lift this span to a span from \(S\) to \(T\) and thus \(S\) and \(T\) are in the same connected component.
\end{proof}

Before we continue to follow \cite{sattlerIdempotentCompletionCubes2019}, we need yet another lemma about lifting elegant Reedy
structures. Sadly this does not work well for Eilenberg-Zilber categories. So we need to find a way around this later.

\begin{lemma}\label{liftReedyToComma}
	Let \A be an elegant Reedy category, \(i : \A → \B \) a functor and \(B ∈ \B \) an object in \B. We can lift
	the elegant Reedy structure along \(p : B ↓ i → \A \), where \(p\) is the evident projection from the comma
	category.
\end{lemma}
\begin{proof}
	First we need to define a degree function \(\d: \Obj (\B) → ℕ\), let \(\d'\) be the degree function from the elegant Reedy structure
	we can then define \(\d ≔ \d'p\). We define the degeneracies and faces, as being degeneracies and faces under \(p\).
  Here we would already get a problem with EZ-categories as we might have maps that are monic in \(B ↓ i\), but not in \B.
	
	As a next step we need to construct the desired factorization into a degeneracy and a face map. So we take
	a map \(f\) in \(B ↓ i\) and factor it as a map in \A into \(f = f_f f_d\). If we try to lift the factorization
	we end up with the following diagram:
	\begin{eqcd*}
		{} & B \arrow[dl, "ϕ"'] \arrow[dr, "ϕ'"] & \\
		i(A) \arrow[rr,"i(f)", near start] \arrow[dr, "i(f_d)"'] &      & i(A') \\
		{}   & i(X) \arrow[ur, "i(f_f)"'] \arrow[from=uu, crossing over, "i(f_d)ϕ", near start] &
	\end{eqcd*}
	It remains to show that the front right triangle commutes.
	\begin{equation*}
		i(f_f)(i(f_d)ϕ) = (i(f_f)i(f_d))ϕ= i(f_f f_d) ϕ = i(f) ϕ = ϕ'
	\end{equation*}
	% Is there an error here? The split makes a problem right?
	It is then tedious, but straight forward to check one of the equivalent elegance axioms. 	
\end{proof}

\begin{lemma}\label{commaPullback}
	Let \(i : \A → \B\) be a functor, and \(B\) an object of \(\B\), and let \(p : B ↓ i → A \) be the  projection map. A
	span in \(B ↓ i\) has a pullback, if the span has a pullback in \B, and the pullback square lies in the image of \(i\).
\end{lemma}
\begin{remark}
	Usually this situation is given, if \A has pullbacks along a class of maps and \(i\) preserves them.
\end{remark}
\begin{proof}
	 So consider a span of  maps in \(B ↓ i\). That fulfills the conditions of this lemma.
	 If we unravel this, we get the following diagram:
	\begin{eqcd*}
		{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] & \\
		{} & & \\
		i(X) \arrow[rd, "i(f)"] & & i(Y) \arrow[ld, "i(g)"'] \\
		{} & i(Z) &
	\end{eqcd*}
	By assumption we have pullbacks of \(i(f)\) and \(i(g)\) in \B that lie in the image of \(i\). So we
	can complete the diagram
	\begin{eqcd*}
		{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] \arrow[d,dashed, "{⟨ϕ,ϕ'⟩}"] & \\
		{} & i(P) \arrow[ld] \arrow[rd] & \\
		i(X) \arrow[rd, "i(f)"] & & i(Y) \arrow[ld, "i(g)"'] \\
		{} & i(Z) &
	\end{eqcd*}
	and exhibit \(i(P)\) as an object in \(B ↓ i\) by the universal map of the pullback.
\end{proof}

\begin{lemma}[{\cite[lemma 3.5]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.5}
	Let \A be an elegant Reedy category and \(i : \A → \B\) a functor. Assume that \A has pullbacks along face maps whenever the
	cospan under consideration lies in the image of the projection \(B ↓ i → \A\) for some \(B ∈ \B\), and that \(i\) preserves these pullbacks.
	Then the left Kan extension \(i_! : \hat{\A} → \hat{\B}\) preserves monomorphisms.
\end{lemma}
\begin{remark}
	The original source also requires that these pullbacks preserve face and degeneracy maps. We get around this by making use of the fact
	that degeneracies are split in \cref{lem:liftEZFib}.
\end{remark}
\begin{proof}
	We only need to show that \(i_!\) preserves monomorphisms component wise, giving us a functor from \(\hat{\A} → \Set\) for every
	object in \( B ∈\B\). This functor can be written as
	\begin{eqcd*}
		\hat{\A} \arrow[r,"p^*"] & \widehat{B ↓ i} \arrow[r,"\colim"] & \Set
	\end{eqcd*}
	where \(p : B ↓ i → \A\) is the projection.
	This is the usual construction of \(i_!\) in this setting, see for example \cite{stacks00VC}.
	It is trivial that \(p^*\) preserves monomorphisms, so we only need to check that \(\colim\) does.
	We want to apply \cref{lem:idemLemma3.4}.
	We can lift the elegant Reedy structure from \A to \( B ↓ i \) along \(p\) by \cref{liftReedyToComma}.
  And as the face maps in \(B↓i\) are defined as maps that \(p\) sends to face maps in \A. We can lift the
  required pullbacks to \(B↓i\) by \cref{commaPullback}.
\end{proof}


\begin{proof}[Proof of \cref{prop:i!preservesMonos}]
	We want to verify the conditions for \cref{lem:idemLemma3.5}. Our first observation is that \(Δ\) does not have arbitrary
	pullbacks of face maps. Intuitively speaking we have only the non-empty ones. So let us unpack the condition that
	we only need pullbacks if the cospan of face maps lies in the image of the projection \(B ↓ i → Δ\) for some \(B\).
	That means there is a \(B ∈ \FL\) such that the following square commutes:
	\begin{eqcd*}
		{} & B \arrow[rd] \arrow[ld] & \\
		i(X) \arrow[rd, "i(f_f)"] & & i(Y) \arrow[ld, "i(g_f)"'] \\
		{} & i(Z) &
	\end{eqcd*} %COMMENT
	As the face maps in \(Δ\) are monic, we can identify \(X\) and \(Y\) with their respective image in \(Z\). As \FL does not
	contain the empty poset, they share at least a point, and the pullback is given by \(\im f_f ∩ \im g_f\). A quick calculation
	shows that this is also a pullback in \FL and thus we can apply \cref{lem:idemLemma3.5} 
\end{proof}


\subsection{\(j^*\) and \(j_!\) are left Quillen}
We are now going to show that \(j^*\) and \(j_!\) are left Quillen. As expected, the hard part will be again to show that
\(j_!\) preserves monomorphisms.

So let us start with \(j^*\) again.

\begin{proposition}\label{prop:j*preservesMonos}
	\(j^*\) preserves monomorphisms.
\end{proposition}
\begin{proof}
	Follows directly from \cref{lem:restrictionPreserveMonos}
\end{proof}

\begin{proposition}\label{prop:j^*preservesTrivialCofib}
	\(j^*\) preserves trivial cofibrations.
\end{proposition}
\begin{proof}
	Like in \cref{prop:i*preservesTrivialCofib}, we are in the comfortable position of being left and right adjoint.
	Note that \(j^*\) also preserves the interval inclusion. As pushout products with the interval inclusion send cofibrations
	to trivial cofibrations and \(j^*\) preserves monomorphisms by \cref{prop:j*preservesMonos}, \(j^*\) sends trivial cofibrations
	to trivial cofibrations.
\end{proof}

\begin{proposition}\label{prop:j!preservesTrivialCofib}
	\(j^*\) preserves fibrations
\end{proposition}
\begin{proof}
	Preservation of uniform fibrations is clear, as every lifting problem against a generating trivial cofibration factors
	throug the image of a trivial cofibration under \(j^*\). As \(j^*\) preserves coequalizer the equivariance follows
	from the equivariance of the model category on \dcSet, which follows from the presence of (at least one connection).
\end{proof}\todo{define uniform fibrations without equivariance}\todo{make a lemma that \dcSet is equivariant even if we just cite this from the relative elegance paper}

We want to recap the general proof idea that \(i_!\) preserved monos. We can test being a monomorphism component wise and can write the
left Kan extension evaluated at a point as some mono preserving functor followed by a colimit.
That the colimit preserves  monomorphisms is equivalent to a condition of connected components on the categories
of elements. We can only lift morphisms backwards along discrete Grothendieck fibrations, but we are faced
with zigzags. To remedy this we want to lift a strong enough pullback property to turn these zigzags into spans.

This strategy will be the same for \(j_!\). Sadly we couldn't get arbitrary Eilenberg-Zilber structures to lift, so
we will need a slightly different attack point.

We first observe that \(□\) has a lot more pullbacks then \(Δ\). While \(Δ\) has only “non-empty” pullbacks of face maps,
\(□\) has all “non-empty" pullbacks. This elevates us from the necessity to lift the Eilenberg-Zilber structure to \(B ↓ i\).
We can get by with the following lemma.

\begin{lemma}\label{lem:pullbackMono}
	Let \(i: \A → \B\) be a functor such that for all \(B ∈ \B\), spans in the image of the projection \(p: B ↓ i\) have pullbacks
	in \B, and these pullbacks are in the image of \(i\). Then \(i_!\) preserves monomorphisms.
\end{lemma}

To show this we replace \cref{lem:idemLemma3.4} with the following simpler lemma.

\begin{lemma}\label{lem:colimPullbackMono}
Let \C be a category. Assume \C has pullbacks, then the functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
\end{lemma}
\begin{proof}
	Again let \(f\) be a monomorphism in \(\hat{\C}\). This is equivalently a monomorphism \(F: P → Q\) of discrete Grothendieck fibrations
	over \C. We need to show that \(F\) is injective on connected components. We can lift the pullbacks to \(Q\) by \cref{lem:liftPullbacks}.
	Let now \(S\) and \(T\) be in \(Q\) such that \(F(S)\) and \(F(T)\) are connected by a zigzag. We can turn this zigzag into a span, by
	taking pullbacks of cospans. Because \(F\) is monic it is injective on objects and we can lift this span to a span in \(P\) and thus
  \(S\) and \(T\) are in the same connected component.
\end{proof}

\begin{proof}[Proof of \cref{lem:pullbackMono}]
	As in \cref{lem:idemLemma3.5}, we check that \(i_!\) preserves monos component wise. We write \(i_!(B)\) again as
	\begin{eqcd*}
		\hat{\A} \arrow[r, "p^*"] & \widehat{B ↓ i} \arrow[r, "\colim"] & \Set
	\end{eqcd*}
	where \(p : B ↓ i → A\) is the projection map. We need to show that \(B ↓ i\) has pullbacks, but that is an immediate
	consequence of \cref{commaPullback}.
\end{proof}

And we arrive at the conclusion we wanted to get to:
\begin{lemma}
	Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B} → \hat{\A}\) preserves monomorphisms.
\end{lemma}

\begin{proposition}\label{prop:j!preservesMonos}
	\(j_! : \widehat{\FL} → \□\) preserves monomorphisms.
\end{proposition}
\begin{proof}
	For this proof we will identify \(2 = \{⊥,⊤\}\).
	We want to fulfill the conditions of \cref{lem:pullbackMono}. To check these conditions, we check that equalizers and products
	with the desired conditions exist. Products are a straightforward calculation so we go forward to the equalizer case.
	To check this we will look at a diagram of the following form,
	\begin{eqcd*}[column sep=small]
		{} & B \arrow[ld] \arrow[rd] & \\
		𝟚^n \arrow[rr, "j(f)", shift left] \arrow[rr, "j(g)"', shift right] & & 𝟚^m
	\end{eqcd*}
	where we identify \(f\) and \(g\) with functions \(m → n + 2\).
	We note that equalizers, if they exist in \FL, are constructed the same way as in \Set.
	If we apply this to our diagram, we can see that this construction can't create something empty,
	as both maps needs to preserve elements from \(B\).
	We would like to complete the diagram in the following way
	%\begin{eqcd*}[column sep=large]
	\begin{equation*}
		\begin{tikzcd}[column sep=large]
		{} & B \arrow[dl] \arrow[d] \arrow[dr] & {} \\
		𝟚^l \arrow[r,"j(e)"] & 𝟚^n \arrow[r,"j(f)", shift left] \arrow[r,"j(g)"',shift right] & 𝟚^m
		\end{tikzcd}
	\end{equation*}
	So we need to find a finite set \(l\) and a map \(e : n → l + 2\). We will construct those by
	effectively constructing the coequalizer in \FinSet. So we take the quotient \(\faktor{n+2}{\sim}\)
	where \(\sim\) is the equivalence relation generated by the relation of having a joint preimage under
	\(f\) and \(g\). We will now argue that our equalizer would be empty if this quotient identifies
	\(⊤\) and \(⊥\).

	We assume that indeed the relation identifies \(⊥\) and \(⊤\), let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\).
	Because \(⊥\) and \(⊤\) are being identified, there exists two finite sequence of elements \(x_i\) and \(y_i\) in \(m\), such that
	there exists a \(k\) and
	(WLOG) \(f(x_1) = ⊥\), \(g(x_i) = f(y_i)\), \(g(y_i) = f(x_{i+1})\) and \(g(y_k) = ⊤\).
	Plugging that into the definition of \(j\), we get
	\begin{align*}
		⊥  = j(f)(h)(x_1) &= j(g)(h)(x_1) = j(f)(h)(y_1) \\ &= j(g)(h)(y_1) = j(f)(h)(x_2) = … = j(g)(h)(y_k) = ⊤
	\end{align*}
	which is a contradiction and thus \(⊤\) and \(⊥\) are not identified.
	For \(e : n → l + 2\), we take the evident quotient map restricted to \(n\).
	While we now have our candidate, we still need to show that this is actually a pushout in \FL. As \FL is well pointed
	it suffices to check global elements, which again are just elements in the set theoretic sense.
  As \(fe = ge\) by construction and \(j\) is a functor we get \(j(f)j(e) = j(g)j(e)\).

  Again let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\). We can then define
  \begin{align*}
  h': l → 𝟚 && \text{by} && h'(x) ≔ h(z) & & \text{where} && z ∈ e^{-1}(x)\text{.}
  \end{align*}
  For this definition to make sense we need to argue that the choice of \(z\) does not matter.
  So let \(z\) and \(z'\) be both element of \(e^{-1}(x)\). Like above that means there are
  two sequences \(x_i\) and \(y_i\) like above, just that \(f(x_1) = z\) and \(g(y_k) = z'\), instead
  of \(⊥\) and \(⊤\).
  And like above we get
  \begin{align*}
  h(z) = j(f)(h)(x_1) &= j(g)(h)(x_1) = j(f)(h)(y_1) \\ &= j(g)(h)(y_1) = j(f)(h)(x_2) = … = j(g)(h)(y_k) = h(z')
  \end{align*}
  We also need that the map \(j(e)\) is monic, but this follows directly from the fact that \(e\) in \FinSet is epic.
  We only need to produce a map \(B → 𝟚^l\), that commutes. We get this map directly, because we have shown that
  this diagram is an equalizer in \FL.
	This means we fulfill the conditions of \cref{lem:pullbackMono} and thus \(j_!\) preserves monomorphisms.
\end{proof}

\subsection{\(i^*j_!\) and \(j^*i_!\) induce an equivalence of homotopy categories}
Before we continue our plan directly, we take a short detour to get a little bit better idea how these two functors behave.

From the previous sections it is immediately clear that \(i^*j_!\) and \(j^*i_!\)  are left Quillen functors with some right adjoint.
One might ask if these two functors are adjoint to each other. The former development would suggest that they aren't
and that is indeed the case.

\begin{definition}\label{def:triangulation}
	Let \(t: □ → \Δ\) be the functor that sends \([1]^n \mapsto (Δ^1)^n\). The \emph{triangulation functor \(\T\)}
	is the left Kan extension of \(t\) along Yoneda.
	\begin{eqcd*}
		□ \arrow[r,"t"] \arrow[d,"\Yo"] & \Δ \\
		\□ \arrow[ru,"\T"] & 
	\end{eqcd*}
\end{definition}

\begin{proposition}\label{prop:triangulation}
	The functor \(i^*j_!\) is the triangulation functor.
\end{proposition}
\begin{proof}
	As \T is the unique cocontinuous functor that extends the product preserving functor from \□ to \Δ that sends the interval
	to the interval, we only need to show these conditions. \(i^*j_!\) is cocontinuous as it is the composition of two left
	adjoints. We need to show that this functor is product preserving on representables. But by Yoneda and \cref{prop:j_!Nothing}
	\begin{equation*}
		j_!(\I^n × \I^m) = j_!(\I^{n+m}) = \Yo 𝟚^{n+m} = \Yo 𝟚^n × \Yo 𝟚^m = j_!(\I^n) × j_!(\I^m)
	\end{equation*}
	\(j_!\) preserves products of representables.
	Because \(i^*\) is a right adjoint we get this property immediately. We also need to show that \(i^*j_!\) preserves the interval.
	We already know this for \(j_!\). So the question is if \(i^*\) preserves the interval. We now that \(i^*(\I)(x) =
	\Hom_{\dCube}(\Yo [1],i(x))\). As \(i\) is fully faithful the claim follows.
\end{proof}

\begin{example}
	\begin{equation*}
		\Hom_{\□}(j^*i_!(Δ^2),\I^2) ≠ \Hom_{\Δ}(Δ^2,i^*j_!(\I^2))
	\end{equation*}
\end{example}%
Intuitively the reason for this is that we can't map a square with one side degenerated to a triangle into the representable
square in \□. But we have a lot of ways to map a triangle into a triangulated square in \Δ.
\begin{proof}
	By the Yoneda lemma and that \(j^*i_!\) is the triangulation functor, a map on the right-hand side corresponds to a
	pair of monotone maps \([2] → [1]\). There are 16 of such pairs. On the left we can use \cref{prop:j_!Nothing},
	and expanding the definition to get \(\Hom_{\□}(\Hom_{\FL}(j(-),[2]),\Hom_{□}(-,2))\). Lets take such a transformation
	and call it \(η\). \(η_0\) gives rise to a map \(f : [2] → 𝟚^2\). \(η_1\) witnesses that \(f\) is indeed monotone, by
	composing with face maps. And \(η_2\) rules out all injective maps, as for them always exactly 2 faces agree and
	\(\I^2(2)\) does not contain such faces. There are only 9 such maps, which is an upper bound for the possible number of
	natural transformations.
\end{proof}

\begin{example}
	\begin{equation*}
		\Hom_{\Δ}(i^*j_!(\I^2),Δ^1 × Δ^1) ≠ \Hom_{\□}(\I^2,j^*i_!(Δ^1 × Δ^1))
	\end{equation*}
\end{example}%
Here the problem is that the square made from a product in \Δ doesn't have a 2-cell that fills the whole square, this
doesn't give us a way to map the representable square on it without degenerating something. While if we triangulate the representable square
first we don't run into that problem. 
\begin{proof}
	As \(j^*i_!\) is the triangulation functor, the left-hand side becomes \(\Hom_{\Δ}(Δ^1 × Δ^1,Δ^1 × Δ^1)\).
	We can write \( Δ^1 × Δ^1 \) as a pushout of two copies of \(Δ^1\) joint by an edge.
	As \(i_!\) is cocontinuous, we can construct this pushout in \FL. By this and \cref{prop:i_!Nothing}, we
	get a colimit of two representables there. Unraveling these definition it is a straightforward exercise
	to verify that the set of on the left-hand side has more elements.
\end{proof}

From here on we follow the argument from \cite[§6.2]{solution}. They lay down a criterion on functors and model categories
such that every natural transformation between them is a weak equivalence. Thus we only need to construct any natural
transformation between the identity functor and the concatenation of these functors.

For this, we cite two technical
lemmas whose theory is mostly developed in \cite{riehlTheoryPracticeReedy2014}, but are taken in this form from \cite{solution}.
To make sense of the first lemma we need
to introduce a technicality. If we have a category \A and presheaves on it, then the automorphism group of some
\(a ∈ \A\) acts on \(\Yo a\,b\) by composition. This kind of acting is natural in the sense that \(\Yo a f\) is an
\(\mathrm{Aut}(a)\)-equivariant map. Thus we can say \(\mathrm{Aut}(a)\) acts on \(\Yo a\). And thus we can also
quotient \(\Yo a\) by subgroups of \(\mathrm{Aut}(a)\). This is also where equivariance comes into play again, as
equivariance by definition guarantees us that these quotients of representables by some automorphism subgroup are
contractible.

\todo{if time and resources explain and proof these lemma (ca. 4 pages)}
\begin{lemma}[{\cites[§5]{riehlTheoryPracticeReedy2014}[lemma 6.2.13]{solution}}]\label{lem:Eilenberg-ZilberMonosCreated}
	Let \A be an Eilenberg-Zilber category. Then the monomorphisms in \(\hat{\A}\) are generated under
	coproduct, pushout, sequential composition, and right cancellation under monomorphisms by the maps
	\(­­∅ → \faktor{\Yo a}{H}\) valued in the quotient of a representable presheaf at some \(a ∈ \A\) by an arbitrary
	subgroup \(H\) of its automorphism group.	
\end{lemma}

\begin{lemma}[{\cites[§5]{riehlTheoryPracticeReedy2014}[lemma 6.2.15]{solution}}]\label{lem:PairClosure}
	Let \(U,V : K → M\) be a cocontinuous pair of functors valued in a model category and \(α : U ⇒ V\) a
	natural transformation between them. Define the cofibrations in \(K\) to be the  maps that are sent to
	cofibrations under both \(U\) and \(V\). Define \(\mathcal{N}\) to be the class of cofibrations
	between cofibrant objects that are sent by Leibniz pushout application with \(α\) to weak equivalences in
	\(M\). Then \(\mathcal{N}\) is closed under coproducts, pushout, (transfinite) composition, and right cancellation
	between cofibrations.
\end{lemma}

\begin{corollary}[{\cite[corollary 6.2.16]{solution}}]\label{lem:everythingWorks}
	Let \A be an Eilenberg–Zilber category and consider a parallel pair of functors \(U, V : \Set^{\A^\op} → M\) valued in a model
	category \(M\) together with a natural transformation \(α : U ⇒ V\) . Suppose that \(U\) and \(V\) preserve colimits and send monomorphisms
	in \(K\) to cofibrations in \(M\). Then if the components of \(α\) at quotients of representables by subgroups of their automorphism groups
	are weak equivalences, then all components of \(α\) are weak equivalences.
\end{corollary}
\begin{proof}
	By \cref{test}\todo{In Leibniz construction chapter make this an example} we can write the the part of \(α\) at \(X\) as a
	Leibniz application with the monomorphism \(∅ → X\). We can use both lemmas from above to show that \(α\) gets send by all
	of those maps to a weak equivalence. By \cref{lem:Eilenberg-ZilberMonosCreated} the monomorphisms in \(\Set^{\A^\op}\) are generated by
	morphisms \(∅ → \faktor{\Yo a}{H}\) under some closure properties. By assumption, morphisms of that form are sent to weak equivalences
	by the Leibniz application with \(α\). By \cref{lem:PairClosure}, the maps that get send to weak equivalences by Leibniz application with
	\(α\) have the same closure properties, thus all monomorphisms get send to weak equivalences, and with them all morphisms of the
	form \(∅ → X\).
\end{proof}

\begin{corollary}[{\cite[Corollary 6.2.17]{solution}}]\label{cor:dafuq}
	Let \A be an Eilenberg–Zilber category for which \(\Set^{\A^\op}\) admits a model structure whose cofibrations are the monomorphisms,
	in which the
	quotients \(\faktor{\Yo a}{H}\) of representables by subgroups of their automorphism groups are weakly contractible. Then if
	\(U, V : \Set^{\A^\op} → M\) define a
	pair of left Quillen functors that preserve the terminal object, then any natural transformation \(α : U ⇒ V\) is a natural weak equivalence.
\end{corollary}
\begin{proof}
	By Ken Browns lemma, left Quillen functors preserve weak equivalences between cofibrant objects. If such a functor preserves the terminal
	object, then it also preserves weak contractibility between cofibrant objects. To apply \cref{lem:everythingWorks}
	we need show that \(α_{\faktor{\Yo a}{H}}\) is a weak equivalence. As this is weakly contractible, we get the following commuting
	square.
	\begin{eqcd*}[column sep=large, row sep=large]
		U\left(\faktor{\Yo a}{H}\right) \arrow[r,"α_{\faktor{\Yo a}{H}}"] \arrow[d, "\rotatebox{90}{\(\sim\)}"] & V\left(\faktor{\Yo a}{H}\right) \arrow[d, "\rotatebox{90}{\(\sim\)}"]  \\
		U(*) \arrow[r,equal] & V(*)
	\end{eqcd*}
	And by 2-out-of-3, the upper map must be a weak equivalence, and thus by \cref{lem:everythingWorks} the claim follows.
\end{proof}

\begin{theorem}
	\(j^*i_!\) and \(i^*j_!\) induce an equivalence between \(\Ho(\□)\) and \(\Ho(\Δ)\).
\end{theorem}
\begin{proof}
	By \cref{prop:i*preservesMonos,prop:i*preservesTrivialCofib,prop:i!preservesMonos,prop:i!preservesTrivialCofib,%
	prop:j!preservesTrivialCofib,prop:j!preservesMonos,prop:j*preservesMonos,prop:j^*preservesTrivialCofib}, are
	\(i^*\),\(i_!\),\(j^*\), and \(j_!\) left Quillen functors, and thus \(j^*i_!\) and \(i^*j_!\) too.
	By Ken Browns lemma we know that left Quillen functors preserve weak equivalences between cofibrant objects. In
	the model structures on \□ and \Δ, every monomorphism a cofibration and thus every object cofibrant.
	Thus \(j^*i_!\) and \(i^*j_!\) preserve weak equivalences and descend to functors between the corresponding
	homotopy categories.

	To show that these induce an equivalence between the homotopy categories we must show that we have a zigzag of
	natural transformations between \(i^*j_!j^*i_!\) and the identity functor such that every natural transformation
	is valued in weak equivalences, and likewise for \(j^*i_!i^*j_!\). We will call \(η^i\) and \(ε^i\) the unit and counit
	of the adjunction \(i_! ⊣ i^*\). Likewise \(η^j\) and \(ε^j\) for the adjunction \(j_! ⊣ j^*\).
	We can construct these as follows
	\begin{eqcd*}[column sep=large, row sep=large,execute at end picture={\draw[decorate,decoration={brace,mirror,amplitude=4.5}] (sBrcs.south) to (eBrcs.south);}]
		\Δ \arrow[r,"i_!", ""'{name=i!s}] & |[alias=sBrcs]| \dcSet \arrow[r,"j^*"] \arrow[d,phantom,"⊛"] \arrow[rr,bend right=20,phantom , ""'{name=cc}] & \□ \arrow[r,"j_!"] & |[alias=eBrcs]| \dcSet \arrow[r,"i^*", ""'{name=i*s}] \arrow[d,phantom,"⊛"] & \Δ \\
		\Δ \arrow[r,"i_!"{name=i!t}] & \dcSet \arrow[rr,"\id"{name=sida},""'{name=sidb}, equal] & & \dcSet \arrow[r,"i^*"{name=i*t}] & \Δ \\
		\Δ \arrow[rrrr,"\id"{name=lid}, equal] & & & & \Δ
		\arrow[Rightarrow ,from=i!s, to=i!t, "\id"]
		\arrow[Rightarrow, from=cc, to=sida, "ε^j"]
		\arrow[Rightarrow, from=i*s, to=i*t, "\id"]
		\arrow[Rightarrow, from=lid, to=sidb, "η^i"]
	\end{eqcd*}
	and
	\begin{eqcd*}[column sep=large, row sep=large,execute at end picture={\draw[decorate,decoration={brace,mirror,amplitude=4.5}] (sBrcs.south) to (eBrcs.south);}]
		\□ \arrow[r,"j_!", ""'{name=j!s}] & |[alias=sBrcs]| \dcSet \arrow[r,"i^*"] \arrow[d,phantom,"⊛"] \arrow[rr,bend right=20,phantom, ""'{name=cc}] & \Δ \arrow[r,"i_!"] & |[alias=eBrcs]| \dcSet \arrow[r,"j^*", ""'{name=j*s}] \arrow[d,phantom,"⊛"] & \□ \\
		\□ \arrow[r,"j_!"{name=j!t}] & \dcSet \arrow[rr,"\id"{name=sida},""'{name=sidb}, equal] & & \dcSet \arrow[r,"j^*"{name=j*t}] & \□ \\
		\□ \arrow[rrrr,"\id"{name=lid}, equal] & & & & \□
		\arrow[Rightarrow ,from=j!s, to=j!t, "\id"]
		\arrow[Rightarrow, from=cc, to=sida, "ε^i"]
		\arrow[Rightarrow, from=j*s, to=j*t, "\id"]
		\arrow[Rightarrow, from=lid, to=sidb, "η^j"]
	\end{eqcd*}
	where \(⊛\) is the Godement product.
	By \cref{prop:i_!Nothing,prop:j_!Nothing}, \(i_!\) and \(j_!\) preserve terminal obejcts and \(i^*\) and \(j^*\) do so because they are
	right adjoints. So by \cref{cor:dafuq} these two cospans of natural transformations are weak equivalences and thus we have our
	desired equivalence of homotopy categories.
\end{proof}
\end{document}
