\documentclass[../Main.tex]{subfiles}
\begin{document}
\section{Name TODO}
This arguments from this section follows very closely/This section recalls \cite[section 3]{cavalloRelativeEleganceCartesian2022}, which is
itself a refinment of \cite{sattlerEquivalenceExtensionProperty2017}. We focus a bit more on the arguments that we actually need
and leave out some remarks about the overall theory.
and establishes a nice critereon for a premodel structure beeing a model structure. This excerpt is mainly included in this document
to be more selfcontained.

\begin{definition}[{\cite[Def. 3.1.1]{cavalloRelativeEleganceCartesian2022} \cite[Def. 2.1.23]{bartonModel2CategoryEnriched2019}}]
Let \(\M\) be a finitely complete and cocomplete category. A \emph{premodel structure} on \(\M\) constist of two
weak factorization system \((C,F_t)\) called cofibrations and trivial fibrations and \((C_t,F)\) called
trivial cofibrations and fibrations on \(\M\) such that \(C_t ⊂ C\) and \(F_t ⊂ F\).
\end{definition}

The data that is missig for a real model structure is the set of weak equivalences \(W\) such that \(C,W,F\) gets to
be a model structure. In the case of a model structure \(W\) would already be determined by the other two classes,
giving us an obvious candidate for \(W\)

\begin{definition}[{\cite[Def. 3.1.3]{cavalloRelativeEleganceCartesian2022}}]
	A morphism in a premodle structure is a \emph{weak equivalence} if it factors as a trivial cofibration followed
	by a trivial fibration. We will call this class \(W(C,F)\).
\end{definition}

One might rightfully ask, what can stop this of beeing a model structure. The good news is, it is only the 2-out-of-3 property.
The other conditions can be shown quite easely

\begin{lemma}[retract argument]\label{retractArgument}\index{retract Argument}
	Consider a composite morphism \(f : X \overset{i}{→} A \overset{p}{→} Y\)
	Then the following holds
	\begin{itemize}
		\item If \(f\) has the left lifting property against \(p\), then \(f\) is a rectract of \(i\).
		\item If \(f\) has the riht lifting property against \(i\), then \(f\) is a retract of \(p\).
	\end{itemize}
\end{lemma}
\begin{proof}
	We prove the first statement, the other second one is dual.
	We can write the decomposition of \(f\) like in the following square and get a lift \(l\) against \(p\).
	\begin{equation*}
		\begin{tikzcd}
			X \arrow[r,"i"] \arrow[d,"f"] & A \arrow[d,"p"] \\
			Y \arrow[r,"\id"] \arrow[ur, dashed, "l"] & Y
		\end{tikzcd}
	\end{equation*}
	Now we can realize \(f\) as a retract as follows.
	\begin{equation*}
		\begin{tikzcd}
			X \arrow[r,"\id"] \arrow[d,"f"] & X \arrow[r,"\id"] \arrow[d,"i"] & X \arrow[d,"f"] \\
			Y \arrow[r,"l"] \arrow[rr, bend right, "\id"'] & A \arrow[r, "p"] & Y
		\end{tikzcd}
	\end{equation*}
\end{proof}
\begin{proposition}[{\cite[Def. 3.1.5]{cavalloRelativeEleganceCartesian2022}}]
\(C_t = C ∩ W(C,F)\) and \(F_t = F ∩ W(C,F)\)
\end{proposition}
\begin{proof}
	We are proving the case for trivial cofibrations the other part is analog.
	Let \(g ∈ C ∩ W(C,F)\), then \(g\) factors into a trivial cofibration \(c\)  followd be a trivial fibration \(f\).
	As \(g\) is also a cofibration, \(g\) has the left lifting property against \(f\) and by lemma \ref{retractArgument}
	is a retract of the trivial cofibration \(c\). As those are closed under retracts \(g\) is a trivial cofibration too.

	The other direction follows from the fact that classes defined by lifting propertys always contain identities.
\end{proof}

We now start to reduce the problem of checking 2-out-of-3. It turns out we do not need to check all possible maps.

\begin{definition}[{\cite[Def. 3.1.7]{cavalloRelativeEleganceCartesian2022}}]
	Given a wide subcategory \(\A ⊆ \E\) of a category \(\E\), we say \(\A\) has left cancellation in \(\E\) (or among maps in \(\E\)) when for every
	composable pair \(g\), \(f\) in \(\E\), if \(gf\) and \(g\) are in \(\A\) then \(f\) is in \(\A\). Dually, \(\A\) has right cancellation in \(\E\)
	when for all \(g\), \(f\) with \(gf\), \(f ∈ \A\), we have \(g ∈ \A\).
\end{definition}

\begin{theorem}[{\cite[Thm 3.1.8]{cavalloRelativeEleganceCartesian2022}}]
	\(W(C,F)\) satisfies 2-out-of-3 exactly if the following hold:
	\begin{enumerate}
		\item[(A)] trivial cofibrations have right cancellation among cofibrations and trivial fibrations have left cancellation among fibrations;
		\item[(B)] every (cofibration, trivial fibration) factorization or (trivial cofibration, fibration) factorization of a weak equivalence is
		a (trivial cofibration, trival fibration) factorization;
		\item[(C)] every composite of a trivial fibration followed by a trivial cofibration is a weak equivalence.
	\end{enumerate}
\end{theorem}
\begin{proof}
	Assume \(W(C,F)\) satisfies 2-out-of-3. Let us start with (A), let \(g\) and \(f\) be cofibrations such that \(gf\) and \(g\) are trivial.
	then by 2-out-of-3 \(f\) is a trivial map too. (The second half of (A) follows in the same way) 
	Let us investigate (B). Let \(k\) be a weak equivalence, and \(fg\) be a factorization into a trivial cofibration \(g\) followed by a
	fibration \(f\). Then by 2-out-of-3 \(f\) is a weak equivalence two. (The second half of (B) is analog)
	(C) follows even more directly from 2-out-of-3.

	Let us now assume A-C, and let \(g : Y → Z\) and \(f : X → Y\). We can then factor f into a cofibration followed by a trivial fibration
	and \(g\) into a trivial cofibraiton followed by a fibration.
	\begin{equation*}
		\begin{tikzcd}
			X \arrow[dr, "f"] \arrow[r, tail] & U \arrow[r, tail, "\sim"] \arrow[d,two heads, "\sim"] & W \arrow[d,two heads,"\sim"] \\
			  & Y \arrow[dr, "g"] \arrow[r,tail,"\sim"] & V \arrow[d,two heads] \\
			  &   & Z
		\end{tikzcd}
	\end{equation*}
	The maps from and to \(W\) can be obtained by factorizing the composition \(U \overset{\sim}{→} Y \overset{\sim}{→} V\) again and using (B).
	Now let us suppose \(f\) and \(g\) are weak equivalences, by (B) the maps from \(X → U\) and \(V → Z\) become weak equivalences too.
	Thus the the composition of \(gf\) is a weak equivalence, witnessed by the upper and right side of the diagram.
	Now let us assume that \(f\) and \(gf\) are weak equivalences. By (B) the map \(X → U\) gets to be a trivial cofibration again.
	Thus the composite \(X → W\) is a trivial cofibration and again by (B) the composite map \(W → Z\) gets to be a trivial fibration,
	as these to composites factor \(gf\). By (A) this makes the map \(V → Z\) a trivial fibration. This establishes that \(g\)
	factors as a trivial cofibration by a trivial fibration and hence \(g\) is a weak equivalence.
	The proof for \(g\) and \(gf\) beeing weak equivalences is dual.
\end{proof}

Now we move on and make use of extra structure that (for example) cubical models exhibit. An adjoint functorial cylinder.
\begin{definition}[{\cite[Def. 3.2.1]{cavalloRelativeEleganceCartesian2022}}]\index{functiorial cylinder}
	A \emph{functorial cylinder} on a category \E is a functor \(\I⊗(−): \E → \E \) equipped with \emph{endpoint} and \emph{contraction}
	transformations fitting in a diagram as shown:
	\begin{equation*}
		\begin{tikzcd}[column sep=large, row sep=large]
			\Id \arrow[r, dashed, "δ_0⊗(−)"] \arrow[dr, "\id"] & \I⊗(−) \arrow[d,dashed,"ε⊗(−)" description] & \Id \arrow[l,dashed, "δ_1⊗(−)"'] \arrow[dl,"\id"'] \\
			 & \Id &
		\end{tikzcd}
	\end{equation*}
	An \emph{adjoint functorial cylinder} is a functorial cylinder such that \(\I ⊗ (−) \) is a left adjoint.
	The dual notion is called a \emph{functorial path object} consisting of a functor \(\I ⊘ (−)\) and natural
	transformation \(δ_k ⊘ (−)\) and \(ε ⊘ (−)\).
\end{definition}

\begin{definition}[{\cite[Def. 3.2.2]{cavalloRelativeEleganceCartesian2022}}]
	Given a functiorial cylinder in a cocomplete category, we have a induced \emph{boundary} transformation
	\( ∂ ⊗ X ≔ [δ_0 ⊗ X, δ_1 ⊗ X] : X ⊔ X → \I ⊗ X \).
\end{definition}

\begin{definition}[{\cite[Def. 3.2.4]{cavalloRelativeEleganceCartesian2022}}]
	Write \(@ : [\E,\Cat{F}] × \E → \Cat{F}\) for the application bifunctor definde by \(F @ X ≔ F(X)\).
	Given a category \E with a functorial cylinder and \(f ∈ \E^→\), we abbreviate \((δ_k ⊗ (−)) \hat{@} f : \E^→ → \E^→\)
	as \(δ_k\⊗f\). We likewise write \(ε \⊗ f\) for Leibniz application of the contraction. We write \(δ_k \hat{⊘}(−)\) and
	\(ε \hat{⊘}(−)\) for the dual operations associated to a functorial path object.	
\end{definition}

\begin{definition}[{\cite[Def. 3.2.5]{cavalloRelativeEleganceCartesian2022}}]\index{cylindrical premodel structure}
	A \emph{cylindrical premodel structure} on a category \E consists of a premodel structure and adjoint functorial cylinder on
	\E that are compatible in the following sense:
	\begin{itemize}
		\item \(∂ \⊗ (−)\) preserves cofibrations and trivial cofibrations;
		\item \(δ_k\⊗(−)\) sends cofibrations to trivial cofibrations for \(k ∈ \{0,1\}\).
	\end{itemize}
\end{definition}

TODO Move this to the part about the cube category
\begin{theorem}
	\□ has an adjoint functorial cylinder given by \(\I × (-)\) making the premodel structure giving by the weak factorization system
	in section \ref{modelStructure}, a cylindrical model structure
\end{theorem}
\begin{proof}
	As \□ is a presheaf category and as such cartesian closed, we get \(\I × (−) ⊣ (−)^{\I}\). We also have
	\(δ_k⊗(−) ≔ δ_k × (−)\) and \(ε⊗(−) ≔ ε × (−)\). As the cofibrations are just the monomorphisms, it is clear
	that \(∂\⊗(−)\) preserves cofibrations.
	TODO write out rest (see note cylinder)
\end{proof}

In a cylindrical modelcategory we can 

%AFH compositions
%com : (s : I) → (A s)[φ |-> f * s]  fst(com r) = fst x_0
%CCHM composition
%com : ( A ε)[φ |-> f * ε]
% see CMS20 (Unifying Cubical Models of Univalent type theory
\end{document}
