tired and scared

src/Main.tex

@@ -129,6 +129,10 @@
 \newcommand*{\TFF}{\ensuremath{\mathrm{TF}}\xspace}
 \newcommand*{\CF}{\ensumermath{\mathrm{CF}}\xspace}
 \newcommand*{\Ct}{\ensuremath{\mathcal{C}_t}\xspace}
+\newcommand*{\U}{\ensuremath{\mathcal{U}_κ}\xspace}
+\newcommand*{\Ud}{\ensumermath{\dot{\mathcal{U}}_κ}\xspace}
+\newcommand*{\V}{\ensuremath{\mathcal{V}_κ}\xspace}
+\newcommand*{\Vd}{\ensuremath{\dot{\mathcal{V}}_κ}\xspace}
 
 \newcommand*{\Hom}{\mathrm{Hom}}
 \newcommand*{\Ho}{\mathrm{Ho}}
@@ -148,9 +152,9 @@
 \renewcommand*{\d}{\mathsf{d}}
 \renewcommand*{\i}{\textsf{i}}
 \renewcommand*{\t}{\mathsf{t}}
-\newcommand*{\⊗}{\mathbin{\hat{⊗}}}
+\newcommand*{\⊗}{\mathbin{\widehat{⊗}}}
-\newcommand*{\×}{\mathbin{\hat{×}}}
+\newcommand*{\×}{\mathbin{\widehat{×}}}
-\newcommand*{\at}{\mathbin{\hat{@}}}
+\newcommand*{\at}{\mathbin{\widehat{@}}}
 \newcommand*{\□}{\ensuremath{\widehat{□}}\xspace}
 \newcommand*{\Δ}{\ensuremath{\widehat{Δ}}\xspace}
 \newcommand*{\dCube}{\ensuremath{□_{∧∨}}\xspace}

src/Preliminaries/Model_Structure.tex

@@ -11,15 +11,15 @@
 We now presenting our, main star, the equivariant model structure on cubical sets.
 We will give a description of the two involved factorization systems and then follow
 an argument from \cite{cavalloRelativeEleganceCartesian2022}, to show that it is indeed
-a model structure. The modelstructure as well as the presentation is taken from
+a model structure. The model structure as well as the presentation is taken from
 \cite{riehlVid}. This
 equivariant model structure is also know as the ACCRS model structure.
 
 % reference for uniform fibrations CCHM and 
 The “usual” model structure on this cube category is not equivalent to spaces, as shown
 by Buchholtz. %TODO find citation
-If we build the qutoient by swapping the dimensions of a square, the resulting space is not
+If we build the quotient by swapping the dimensions of a square, the resulting space is not
-contractable, while in spaces it is. The idea is to correct this defect, by making the embedding
+contractible, while in spaces it is. The idea is to correct this defect, by making the embedding
 of the point a trivial cofibration. This is archived by forcing an extra property onto
 the fibrations.
 
@@ -30,8 +30,8 @@ the fibrations.
 \end{tikzcd}
 \end{equation*} % Fix twist of suboject
 
-Here \(σ\) is the map that swaps the dimenisons and  \(e\) is the coequilizer map. The hope would be, that
+Here \(σ\) is the map that swaps the dimensions and  \(e\) is the coequalizer map. The hope would be, that
-the coequilizer, would now present a lift for the right most lifting problem. But in general that
+the coequalizer, would now present a lift for the right most lifting problem. But in general that
 does not hold, the lifts have neither to commute with \(σ\) nor with \(\id\). The path forward
 will be to restrict the fibrations to have the desired property.
 %
@@ -39,10 +39,10 @@ will be to restrict the fibrations to have the desired property.
 % \subsubsection{Weak factorization systems}
 % If we force additional properties on our lifting problems, one might rightfully
 % ask if these indeed induce a weak factorization system (wfs). It is also unclear if
-% there are induced factorizations at all. The good news is, there is a refined version
+% there are induced factorization at all. The good news is, there is a refined version
 % of the small object argument \cref{smallObject}, that will help us out. This works on
 % the back of algebraic weak factorization systems. We don't need the whole theory and
-% get by with the following definitiont.
+% get by with the following definition.
 % 
 % \begin{definition}\label{def:rightMaps}
 % 	Let \J be category and \(J : \J → \M^→\) be a functor. Then an object \(f\) in
@@ -65,14 +65,14 @@ will be to restrict the fibrations to have the desired property.
 % \end{definition}
 % 
 % \begin{remark}
-% 	If we start with a set \J and make it into a discret category, then we will get our old definition
+% 	If we start with a set \J and make it into a discrete category, then we will get our old definition
 % 	of right lifting map, with an additional choice function for lifts. Which exists anyway if we
 % 	are ready to believe in strong enough choice principles.
 % \end{remark}
 % 
 % After we defined a class of right maps by those lifting problems, it is not clear that these
 % will yield a wfs. 
-% To get those we invoke a refinment of Quillens small object argument, namely
+% To get those we invoke a refinement of Quillens small object argument, namely
 % Garners small object argument \cite{garnerUnderstandingSmallObject2009}. This has the additional benefit of producing
 % algebraic weak factorization systems (awfs). For a quick reference see
 % \cite{riehlMadetoOrderWeakFactorization2015a}, and for an extensive tour \cite{riehlAlgebraicModelStructures2011}, or
@@ -80,7 +80,7 @@ will be to restrict the fibrations to have the desired property.
 % us is the following theorem \cite[][Theorem 2.28]{riehlAlgebraicModelStructures2011}
 % 
 % \begin{theorem}[Garner]\label{smallObject}
-% 	Let \(\M\) be a cocomplete category satisfying either of the following conditions.
+% 	Let \(\M\) be a co-complete category satisfying either of the following conditions.
 % 	\begin{itemize}
 % 		\item[(\(*\))] Every \(X ∈ \M\) is \(α_X\)-presentable for some regular cardinal \(α_X\).
 % 		\item[(\dagger)] Every \(X ∈ \M\) is \(α_X\)-bounded with respect to some proper, well-copowered
@@ -89,8 +89,8 @@ will be to restrict the fibrations to have the desired property.
 % 	Let \( J : \mathcal{J} → \M^→\) be a category over \(\M^→\), with \(\mathcal{J}\) small. Then the free awfs on \(\mathcal{J}\) exists
 % 	and is algebraically-free on \(\mathcal{J}\).
 % \end{theorem}
-% Without going to much into the size issues, every locally presentable categoy satisfies \((\ast)\). And as \(\□\) is a presheaf
+% Without going to much into the size issues, every locally presentable category satisfies \((\ast)\). And as \(\□\) is a presheaf
-% category over a countable category, it is locally presentable. Also by beeing a presheaf category makes it automatically cocomplete.
+% category over a countable category, it is locally presentable. Also by being a presheaf category makes it automatically co-complete.
 % 
 % We also won't clarify all the consequences that getting an awfs instead of a wfs, brings with it. For us the important
 % thing is, that every awfs has an underlying wfs. The free part of that statement unsures that this construction preserves
@@ -103,42 +103,43 @@ will be to restrict the fibrations to have the desired property.
 \subsubsection{Cofibrations and trivial fibrations}
 The short way of specifying this weak factorization system, is by saying
 the cofibrations are the monomorphisms. Another, longer way, but for the further development more
-enlightening is by formulating this as uniform lifting properties.
+enlightening is by formulating this as a uniform lifting properties.
 It is also not equivalent from the viewpoint of an awfs, as this definition has extra conditions on the
 chosen lifts.
 The condition to have uniform lifts, comes from \cite{CCHM} and generalized in \cite{gambinoFrobeniusConditionRight2017} . This requirement is motivated to have
-constructive interpretation of Cubical type theory\todo{see ctt intro chapter when it is done}. As we don't focus on the typetheoretic interpretation, but on the model structure we won't
+constructive interpretation of Cubical type theory\todo{see ctt intro chapter when it is done}. As we don't focus on the type theoretic interpretation, but on the model structure we won't
 explore this further.
 
 \begin{definition}
 	Let \(J : \mathcal{M} ↣ \A^→\) be subcategory which objects are a pullback stable class of morphisms in \A, and morphisms are
-	the cartesian squares between them. The category \(J^⧄\) is called the category \emph{uniform right lifting morphisms} with respect
+	the Cartesian squares between them. The category \(J^⧄\) is called the category \emph{uniform right lifting morphisms} with respect
 	to \(\mathcal{M}\). Objects of \(J^⧄\) are said to have the \emph{uniform right lifting property}.
 \end{definition}
 
 \begin{definition}
-	The category of \emph{uniform generating cofibrations} has as object monomorphisms into a cube \(C ↣ I^n\) of arbitraty dimension, and
+	The category of \emph{uniform generating cofibrations} has as object monomorphisms into a cube \(C ↣ \I^n\) of arbitrary dimension, and
-	as morphism cartesian squares between those.
+	as morphism Cartesian squares between those.
 \end{definition}
 
 \begin{definition}
-	A \emph{uniform trivial cofibration} is a right map with respect to the inclusion functor from the category of uniform generation cofibrations
+	A \emph{uniform trivial fibration} is a right map with respect to the inclusion functor from the category of uniform generation cofibrations
 	into \(\□^→\)
 \end{definition}
 
-\todo{show that the cofib are all monos}
+From this it is not immediately clear that the left maps are all monomorphisms, but it follows from
-
+\cite[Proposition 7.5]{gambinoFrobeniusConditionRight2017}.
-
+By Garners small object argument \cref{awfs:smallObject}, this gives rise to an awfs which we call \((\TCF,\FF)\) and an underlying wfs
+that we call \((\C_t,\F)\)
 \subsubsection{Trivial cofibrations and fibrations}
 
 As we sketched above, the strategy will be to make more maps trivial cofibrations. This is done
 by making it harder to be a fibration. Before we give the definition in full generality, we
-need to adress which coequilizer we talk about percisely.
+need to address which coequalizer we talk about precisely.
 
 Of course doing this only in the 2 dimensional case is not enough. For this we need to say what
-the “swap” maps are. What these should do is permutating the dimensions. So let \(Σ_k\) be the symmetric group
+the “swap” maps are. What these should do is permuting the dimensions. So let \(Σ_k\) be the symmetric group
 on \(k\) elements. For every \(σ' ∈ Σ_k\), we get a map from \( σ : \I^k → \I^k \), by \((π_{σ'(1)}, … , π_{σ'(k)})\),
-where \(π_l : \I^k → \I \) is the \(l\)-th projection. Also if we have a subcube \(f : \I^n \rightarrowtail \I^k\),
+where \(π_l : \I^k → \I \) is the \(l\)-th projection. Also if we have a sub-cube \(f : \I^n \rightarrowtail \I^k\),
 we get a pullback square of the following form
 \begin{equation*}
 	\begin{tikzcd}
@@ -148,11 +149,11 @@ we get a pullback square of the following form
 \end{equation*}
 whose right arrow we call \(σf\).
 %
-Now we desrcibe our generating trivial cofibrations. We remeber example \cref{Leibniz:Ex:OpenBox}. We would
+Now we describe our generating trivial cofibrations. We remember example \cref{Leibniz:Ex:OpenBox}. We would
 like to do the same here, but a bit more general.
 
 
-Instead we are going for boxfillings in the context of a cube. The definition of those will be very similiar
+Instead we are going for box-fillings in the context of a cube. The definition of those will be very similar
 we will just work in the slice over a cube \(I^k\). We do the Pushout-product in the slice, and
 forget the slice to get a map in \(\□\).
 \begin{equation*}
@@ -162,14 +163,14 @@ forget the slice to get a map in \(\□\).
 \end{equation*}
 
 What do we change by working in the slice?
-For intuiton let us first look at the case
+For intuition let us first look at the case
-with a one dimensional context. The point in in this context ist the terminal object in \(\faktor{\□}{\I}\).
+with a one dimensional context. The point in in this context is the terminal object in \(\faktor{\□}{\I}\).
 The interval in this cube category could be described as the pullback, of the interval in \(\□ = \faktor{\□}{\I^0}\)
 along the unique map \(\I → \I^0\), or in simpler words it is the left projection  \(π_l : \I × \I → \I\).
 Let us now look what maps we have from the point into the interval \(\id_\I → π_l \). We get the two
 endpoint maps we expected, as  \(⟨\id, 0⟩ \) and \(⟨\id, 1⟩\), but in this context we get an additional map,
-namely \(⟨\id, \id⟩\). If we would forget the context again (aka beeing in the slice), this is the diagonal of the square. From
+namely \(⟨\id, \id⟩\). If we would forget the context again (aka being in the slice), this is the diagonal of the square. From
-a type theoretic perspective this is realy not surprising. Here it amounts to the question, how many different terms
+a type theoretic perspective this is really not surprising. Here it amounts to the question, how many different terms
 of type \(\I\) can be produced. In an empty context the answer is two.
 \begin{align*}
 	⊢ 0 : \I && ⊢ 1 : \I
@@ -180,7 +181,7 @@ But in the context of \(\I\), the answer is three.
 \end{align*}
 Like the type theory suggest we can think of this, as an generic element of the interval. That this
 element is different from both closed points, is what differentiates the interval from the
-coproduct of two points. In the typetheoretic world we want something that is called a composition structure, and these
+coproduct of two points. In the type theoretic world we want something that is called a composition structure, and these
 should also work
 along those diagonals, this amounts to be able to have be able to have a cube filling property along those diagonals,
 or in other words we want them to be trivial cofibrations too. The earliest mention of the idea the I am aware of is
@@ -189,8 +190,8 @@ this short note \cite{coquandVariationCubicalSets2014}, for a discussion see for
 The generalization of the boundary inclusion is straight forward. We just take any cube over \(\I^k\)
 \(ζ : \I^n → \I^k\) and a monomorphism \(c : C → \I^n\), this also induces an object in the slice by composition.
 Notice that we did not require that \( n ≥ k\).
-If we pack all of this into a definiton we get.
+If we pack all of this into a definition we get.
-\begin{definition}
+\begin{definition}\label{def:modelStructure:generatingTrivialCofibration}
 	Let \(ζ : \I^n → \I^k\) be a cube over \(\I^k\) and \(c : C → \I^n\) monic. A map of the form
 	\begin{equation*}
 		\begin{tikzcd}
@@ -237,7 +238,7 @@ Again we will do this in a slice and forget the slice afterwards.
 	\right)
 \end{equation*}
 Notice that we understand the vertical morphisms as objects of \(\□^→\) and the horizontal ones as morphism in \(\□^→\).
-Also notice, that the left diagramm is a square for which we use in our uniformity condition and the right one captures
+Also notice, that the left diagram is a square for which we use in our uniformity condition and the right one captures
 equivariance. And notice that the pushout-product of the columns yield trivial cofibrations. We will denote the resulting
 commutative square as
 \begin{equation}\label{devilSquare}
@@ -246,7 +247,7 @@ commutative square as
 		\I^m × \I^l \arrow[r, "α×σ"] & \I^n × \I^l
 	\end{tikzcd}
 \end{equation}
-Now we can finaly give the definition of uniform equivariant fibrations.
+Now we can finally give the definition of uniform equivariant fibrations.
 
 \begin{definition}
 	The category of \emph{generating uniform equivariant trivial cofibrations} has as object
@@ -263,19 +264,76 @@ Now we can finaly give the definition of uniform equivariant fibrations.
 	\((\Ct,\F)\)
 \end{notation}
 
-We will show that this is a modelstructure by using the theory of premodel structures
+\subsubsection{The Premodel Structure of Equivariant Cubical Sets}
+On our way to show that this is a model structure, we will use the theory of premodel structures
 \cites{bartonModel2CategoryEnriched2019}[section 3]{cavalloRelativeEleganceCartesian2022}[section 3]{solution}{sattlerCYLINDRICALMODELSTRUCTURES}.
 \todo{if there is time (there probably won't be) include the premodel theory and explain}
-This machinery gives us a nice condition to check if we are actually dealing with a modelstructure. But first we need to
-introduce the notion of a premodel structure.
 
 \begin{definition}[{\cites{bartonModel2CategoryEnriched2019}[def. 3.1.1]{cavalloRelativeEleganceCartesian2022}}]\label{def:preModelStructure}
-	A \emph{premodel Structure} on a finitely cocomplete and complete category \M consists of two weak factorization systems
+	A \emph{premodel Structure} on a finitely co-complete and complete category \M consists of two weak factorization systems
 	\((C,F_t)\) (the \emph{cofibrations} and \emph{trivial fibrations}) and \((C_t, F)\) (the \emph{trivial cofibrations} and \emph{fibrations})
 	on \M such that \(C_t ⊆ C\) (or equivalently \(F_t ⊆ F\) ).
 \end{definition}
 
-And also the definition of a property of such.
+\begin{remark}
+	This structure ascend to all slices and is created by the corresponding forgetful functor. This should not be surprising, as model
+	structures do the same.
+\end{remark}
+
+As all trivial cofibrations are monomorphisms, we get immediately that the two defined factorization systems above form a
+premodel structure. Every premodel structure comes equipped with a notion of weak equivalences.
+
+\begin{definition}[{\cite[Definition 3.1.3]{cavalloRelativeEleganceCartesian2022}}]
+	We say that a morphism in a premodel structure is a weak equivalence if it factors
+	as a trivial cofibration followed by a trivial fibration;
+	we write \(W(C, F)\) for the class of such morphisms.
+\end{definition}
+
+What is missing, is that these equivalences actually satisfy the 2-out-of-3 condition.
+The machinery of premodel structures gives us a nice condition to check if we are actually dealing with a model structure.
+But first we investigate a bit more structure our premodel structure possesses
+
+
+\begin{definition}[{\cite[Definition 3.2.1]{cavalloRelativeEleganceCartesian2022}}]
+	A \emph{functorial cylinder} on a category \(E\) is a functor \(\I⊗(−) : E → E\) equipped with endpoint and contraction
+	transformations fitting in a diagram as shown:
+	\begin{eqcd*}[column sep = large, row sep=large]
+			\Id
+				\arrow[r,"δ_0⊗(−)", dashed]
+				\arrow[dr,"\id"']
+			& \I ⊗ (−)
+				\arrow[d,"ε⊗(−)" description, dashed]
+			& \Id
+				\arrow[l,"δ⊗(−)"',dashed]
+				\arrow[dl,"\id"]
+		\\
+			{}
+			& \Id
+			&
+	\end{eqcd*}
+	An \emph{adjoint functorial cylinder} is a functorial cylinder such that \(I ⊗ (−)\) is a left adjoint.
+\end{definition}
+
+\todo{mention \(ε\) in cubical set notation}
+We can see immediately that the functor \(\I × (−)\) the product with the interval is a functorial cylinder,
+and by \□ being a presheaf topos even an adjoint functorial cylinder. But for now it is not at all clear
+that this functor is relevant in a homotopical sense. This is captured by the next definition.
+
+\begin{definition}[{\cite[Definition 3.2.5]{cavalloRelativeEleganceCartesian2022}}]
+	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{clean up and explain}
+\todo{mention adhesiveness in Leibniz product chapter}
+
+These properties are verified quickly, the map \(∂ : 1 + 1 → \I\) is monic and thus
+it follows from \cref{TODO}. We check the second property on generating cofibrations\todo{is this enough?},
+plugging in the definition of our functorial cylinder we see that this is by definition
+a trivial cofibration if set \(k = 0\) and \(m = 1\) in \cref{def:modelStructure:generatingTrivialCofibration}.
+
 \begin{definition}[{\cite[Definition 3.3.3]{cavalloRelativeEleganceCartesian2022}}]
 	We say a premodel category \M has the fibration extension property when for any fibration
 	\(f : Y → X\) and trivial cofibration \(m : X → X′\), there exists a fibration \(f' : Y' → X'\) whose base change along \(m\) is
@@ -286,18 +344,6 @@ And also the definition of a property of such.
 	\end{eqcd*}
 \end{definition}
 
-\begin{definition}[{\cite[Definition 3.2.5]{cavalloRelativeEleganceCartesian2022}}]
-	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{clean up and explain}
-
-
-We get this characterizing theorem.
-
 \begin{theorem}[{\cite[Theorem 3.3.5]{cavalloRelativeEleganceCartesian2022}}]\label{thm:premodelIsModel} \todo{if this gets longer expanded give it its own section}
 	Let \(\M\) be a cylindrical premodel category in which
 	\begin{enumerate}
@@ -307,10 +353,56 @@ We get this characterizing theorem.
 	Then the premodel structure on \(\M\) defines a model structure.
 \end{theorem}
 
-The first item is fast verified, as all monomorhpisms are cofibrations.\todo{make a small lemma to prove it (closure properties got you covered)}
+The first item is fast verified, as all monomorphisms are cofibrations.\todo{make a small lemma to prove it (closure properties got you covered)}
-The second condition we won't show directly. We will get for free if we construct fibrant universes, which we want to do anyway.
+The second condition we won't show directly. We will get for free if we construct universes, which we want to do anyway.
+% Before we construct universes we will first talk about another property that follows from general
+% pre model structure theory. This property relates back to type theory, as it is the categorical side of
+% glue types. These keep track of type extension and are used to prove univalence. We will use it later to show
+% that the base of our constructed universe is fibrant.
+% In categorical terms it says the following.
+% 
+% \begin{definition}[{\cite{sattlerEquivalenceExtensionProperty2017}}]
+% 	A cylindrical premodel structure has the equivalence extension
+% 	property when any weak equivalence \(e\) over an object \(A\) can be extended along any cofibration
+% 	\(i : A → B\) to a weak equivalence \(f\) over \(B\) with a specified codomain extending that of the original map:
+% 	\begin{eqcd*}
+% 			X_0
+% 				\arrow[rr,dotted]
+% 				\arrow[rd,"e"]
+% 				\arrow[rdd,"p_0"']
+% 			& & Y_0
+% 				\arrow[rd,dashed, "f"]
+% 				\arrow[rdd,dotted]
+% 			&
+% 		\\
+% 			{}
+% 			& X_1
+% 				\arrow[rr, crossing over]
+% 				\arrow[d,"p_1"]
+% 				\arrow[rrd,phantom,"\lrcorner" very near start]
+% 			& & Y_1
+% 				\arrow[d,"q_1"]
+% 		\\
+% 			{}
+% 			& A
+% 				\arrow[rr,"i"]
+% 			& & B
+% 	\end{eqcd*}
+% 	In a setting such as a presheaf topos where we have universe levels,
+% 	there is an additional requirement: for sufficiently large inaccessible cardinals
+% 	\(κ\), if \(p_0\), \(p_1\), and \(q_1\) are \(κ\)-small, so is the extended fibration.
+% \end{definition}
+% 
+% We could have equivalently used \cite[Proposition 5.1]{sattlerEquivalenceExtensionProperty2017},
+% but this version aligns more direct with the data that we are given.
+% \begin{theorem}[{\cite[Theorem 3.3.3]{solution}}]
+% 	Let \(E\) be a locally Cartesian closed category with a cylindrical premodel
+% 	structure in which the cofibrations are the monomorphisms, and these are stable under
+% 	pushout-products in all slices. Then the equivalence extension property holds in \(E\).
+% \end{theorem}
+% The pushout product claim is verified by \cref{TODO}\todo{adhesive note in Leibniz chapter}
 
-\subsubsection{Fibrant Universes}
+\subsubsection{Universes for Fibrations}
 In this section we will change notation between commutative diagrams and the internal language of our presheaf.
 As these tools can get quite technical and tedious to verify, we will only present the idea how these constructions
 work and refer for the technical details to the source material.
@@ -349,16 +441,16 @@ For example by the arguments in \cite[Section 7]{awodeyHofmannStreicherUniverses
 				\arrow[u, "\Fib(f)"']
 	\end{eqcd*}
 \end{definition}
-If the wfs, for that we try to classify the right maps, is functorial we might think of this as an internaliztaion
+If the wfs, for that we try to classify the right maps, is functorial we might think of this as an internalization
-of the \(\R\)-algbera structures on \(f\).
+of the \(\R\)-algebra structures on \(f\).
 
 We will first construct classifying types, after that we construct universes from it.
 
-In preperation of the fibrant case we will first classify the trivial fibrations.
+In preparation of the fibrant case we will first classify the trivial fibrations.
 We don't have any equivariance condition on them, and thus they are the same as in \cite[Section 2]{awodeyCartesianCubicalModel2023},
 when we assume \(Φ = Ω\).
 
-Let us first think about the easiest case where the domain of auf trivial fibration is the terminal.
+Let us first think about the easiest case where the domain of the trivial fibration is the terminal.
 We should ask us what are the \TFF-algebra structures\todo{introduce notion above}. These are intuitively
 choice functions of uniform liftings against cofibrations. So let us think about them first. If we picture
 a lifting problem,
@@ -498,7 +590,7 @@ We now going to extract the classifying type for equivariant cubical fibrations.
 and cubical species. There exists the constant diagram functor \(Δ\) that sends a cubical set to the constant cubical species.
 
 
-Since \□ is complete this functor has a right adjoint\footnote{and also a left adjoint as \□ is cocomplete}
+Since \□ is complete this functor has a right adjoint\footnote{and also a left adjoint as \□ is co-complete}
 \(Γ\) compare \cite[Section 5.1]{solution}, which is given by
 
 \begin{equation*}
@@ -589,7 +681,7 @@ and building the following pullback.
 \end{eqcd*}
 To see this is a fibration we will exhibit we exhibit a split of the classifying type of \(π_κ\).
 As the classifying type is pullback stable we get the following diagram
-\begin{eqcd*}[row sep=large, column sep = large]
+\begin{eqcd*}[]
 		\dot{\mathcal{U}}_κ
 			\pb
 			\arrow[d,"π_κ"]
@@ -611,10 +703,10 @@ As the classifying type is pullback stable we get the following diagram
 The lower pullback square is a pullback of \(\Fib(p)\) along itself. This map has a split, namely the diagonal.
 To show that this classifies small fibrations, let us consider a small fibration \(f : A → X\).
 Because it is a small map we get it as a pull back along a cannonical map \(a : X → \mathcal{V}\).
-\begin{eqcd*}
+\begin{eqcd*}[row sep=small, column sep=small]
 		{}
 		& {}
-		& \dot{\mathcal{U}}
+		& \dot{\mathcal{U_κ}}
 			\arrow[dr]
 			\arrow[dd]
 		&
@@ -623,13 +715,13 @@ Because it is a small map we get it as a pull back along a cannonical map \(a :
 		& |[alias=A]| A
 			\arrow[rr,crossing over]
 			\arrow[ru,dashed]
-		& & \dot{\mathcal{V}}
+		& & \dot{\mathcal{V}_κ}
 			\arrow[dd]
 	\\
 		\Fib(A)
 			\arrow[rr]
 			\arrow[dr]
-		& & \mathcal{U}
+		& & \mathcal{U_κ}
 			\arrow[dr]
 		&
 	\\
@@ -644,17 +736,229 @@ Because it is a small map we get it as a pull back along a cannonical map \(a :
 We get the lower square as a pullback as \Fib is pullback stable and \(\mathcal{U} = \Fib(\dot{\mathcal{V}})\).
 As \(f\) is a fibration, we get a split \(s\) of the fibration structure. And so we get a unique corresponding map
 \(s'\), which induces the required pullback square.
-
 \end{proof}
 
+\begin{definition}[{\cite[Definition 94]{awodeyCartesianCubicalModel2023}}]
+	A map \(P → X\) is said to be a weak proposition if the projection \(P ×_X P → P\) is a trivial fibration.
+	\begin{eqcd*}
+			P^2
+				\arrow[r]
+				\arrow[d]
+				\pb
+			& P
+				\arrow[d]
+		\\
+			P
+				\arrow[r]
+			& X
+	\end{eqcd*}
+	Note that if either projection is a trivial fibration, then both are.
+\end{definition}
+
+\begin{lemma}[{\cite[Lemma 95]{awodeyCartesianCubicalModel2023}}]\label{lem:modelStructure:weakProposition}
+	For any \(A → X\), the classifying type \(\TFib(A) → X\) is a weak proposition. Moreover, the same is true for \(\Fib(A) → X\).
+\end{lemma}
+We again will give the proofidea, sort out the differences for the equivariant case and refer the reader to the
+source material for the technical details.
+\begin{proof}[Proofsketch:]
+	We first prove the case for \(\TFib\) and afterwards reduce the case the \Fib case to it.
+	We first note that if a map \(A → X\) is a trivial fibration, so is \(\TFib(A) → X\). This is
+	because if we expand the definition and look at the \(+\)-algebra structure, the map \(η_x : X → X^+\)
+	is always monic.
+
+	Now let \(f : A → X\) and consider the following diagram.
+	\begin{eqcd*}[column sep=tiny]
+			\TFib(A) ×_X A
+			\arrow[dd]
+			\arrow[rr]
+			& & |[alias=A]| A
+		\\
+			{}
+			& \TFib(A) ×_X \TFib(A)
+				\arrow[dl]
+				\arrow[rr]
+			& & \TFib(A)
+				\arrow[dl]
+		\\
+			\TFib(A)
+			\arrow[rr]
+			& & |[alias=X]| X
+		\arrow[from=A,to=X,crossing over, "f" near start]
+	\end{eqcd*}
+	Since \(\TFib\) is stable under pullback we hav that \( \TFib(\TFib(A) ×_X A) \) is isomporhic to
+	\( \TFib(A) ×_X \TFib(A) \), and since the latter has a canonical section \(\TFib(A) ×_X A → \TFib(A) ×_X \TFib(A)\),
+	the \(\TFib(A) ×_X A\) is a trivial fibration over \(\TFib(A)\). By our note above we see that also \( \TFib(A) ×_X \TFib(A)\) is
+	a trivial fibration over \(\TFib(A)\).
+
+	For \Fib we trace now through the whole construction process, and reduce it to the case above. For the technical details
+	we refer to the source material. For our deviation in the construction we need a few additional properties. Namely
+	the constant diagram functor preserves monomorhpisms, which is obviously true, and that taking exponentials with the
+	interval in cubical species preserves monomorhpisms. As \(Σ\) has only endomorphisms, this reduces again
+	to a componentwise check in \□, where we already know it by \cref{TODO}.\todo{show this}
+\end{proof}
+\begin{remark}
+	The source has an additional condition, that in our setting is true.
+\end{remark}
+
+\begin{lemma}[{\cite[Lemma 96]{awodeyCartesianCubicalModel2023}}]
+	The univeres \(\mathcal{U}_κ\) satisfies \emph{realignment} in the following senes.
+	Given a \(κ\)-small fibration \(g : A → X\) and a cofibration \(c : C → X\), let \(f_c : C → \mathcal{U}_κ\) classify the pullback
+	\(c^∗A → C\). Then there is a classifying map \(f : X ↣ \mathcal{U}_κ\) for \(A\) with \(f c = f_c\).
+	\begin{eqcd*}[row sep = small, column sep = small]
+			c^*F
+				\arrow[rr]
+				\arrow[dr]
+				\arrow[dd]
+			& & \dot{\mathcal{U}}_κ
+				\arrow[dd]
+		\\
+			{}
+			& |[alias=F]| A
+				\arrow[ur,dashed]
+			&
+		\\
+			C
+				\arrow[rr, "f_c" near start]
+				\arrow[rd,tail,"c"]
+			& & \mathcal{U}_κ
+		\\
+			{}
+			& |[alias=X]| X
+				\arrow[ur,dashed,"f"]
+			&
+		\arrow[from=F, to=X, crossing over, "g" near start]
+	\end{eqcd*}
+\end{lemma}
+
+\begin{proof}
+	First, we extend this diagram by the small map classifier and, by realignment for HS-Universes \cref{TODO}\todo{make a lemma, or cite}
+	we get an extension \(f_0\).
+	\begin{eqcd*}[row sep = small, column sep = small]
+			c^*F
+				\arrow[rr]
+				\arrow[dr]
+				\arrow[dd]
+			& & \dot{\mathcal{U}}_κ
+				\arrow[dd]
+				\arrow[r]
+			& \dot{\mathcal{V}}_κ
+				\arrow[dd]
+		\\
+			{}
+			& |[alias=F]| A
+				\arrow[urr,dashed, crossing over]
+			& & 
+		\\
+			C
+				\arrow[rr, "f_c" near start]
+				\arrow[rd,tail,"c"]
+			& & \mathcal{U}_κ
+			\arrow[r]
+			& \mathcal{V}_κ
+		\\
+			{}
+			& |[alias=X]| X
+				\arrow[urr,dashed,"f_0"]
+			& & 
+		\arrow[from=F, to=X, crossing over, "g" near start]
+	\end{eqcd*}
+	Since \(g\) is a fibration we get a lift of \(f_1 : X → \U \) of \(f_0\) classifying the fibration structure.
+	This gives us the following diagram in the base.
+	\begin{eqcd*}
+			C
+				\arrow[r,"f_c"']
+				\arrow[rr,bend left, "\Fib(p)f_c"]
+				\arrow[d, tail, "c"]
+			& \U
+				\arrow[r]
+			& \V
+				\arrow[d, equal]
+		\\
+			X
+				\arrow[r,"f_1"]
+				\arrow[rr, bend right, "Fib(p)f_1"']
+			& \U
+				\arrow[r]
+			& \V
+	\end{eqcd*}
+	We can now pull back \(\Fib(p)\) along itself and rearrenge the data.
+	\begin{eqcd*}
+			C
+				\arrow[d,tail,"c"]
+				\arrow[r,"{⟨f_1c,f_c⟩}"']
+				\arrow[rr,bend left,"fc"]
+			&[3em] \U ×_{\V} \U
+				\arrow[r,"π_2"']
+				\arrow[d,"π_1"]
+			& \U
+				\arrow[d]
+		\\
+			X
+				\arrow[rr,bend right, "f_0"']
+				\arrow[r,"f_1"]
+			& \U
+				\arrow[r]
+			& \V
+	\end{eqcd*}
+	By \cref{lem:modelStructure:weakProposition} \(\Fib(\Vd) = \U → \V\) is a weak proposition, this means
+	\(π_1\) is a trivial fibration and we get a lift \(f_2 : X → \U ×_{\V} \U\), by normal lifting properties.
+	Taking \(f ≔ π_2 f_2\) gives another classifying map for the fibration structure, for which
+	\(fc=f_c\) as required.
+\end{proof}
+
+%This equips us with enough structure to show that the premodel structure above induces indeed a model structure, but
+%from a type theoretic perspective we are not satisfied yet. We want that \(\mathcal{U}\) itself is type, or in categorical
+%words a fibrant object. As we are focusing on the equivalence to spaces right now, this is out of scope of this document
+%and we refer the reader to \cite[Proposition 5.3.9]{solution}.
+\todo{show fibrancy, this is hard and long, but needed for the next part. Or admit defeat and write something here}
+
+
 \todo{introduce Leibniz pullback exponential}
 \todo{introduced (unbiased) uniform fibrations and how they behave with leibniz constructions}
 \todo{hate my life}
 
-\subsubsection{HS-Universe}
+\subsubsection{From Premodel Structure to Model Structure}
-Assume this as given for now, if we have time we can write this out \todo{delete it or write it out, and move it to some preliminary place}
+From here on we assume our constructed universe is fibrant. \todo{hopefully we can get rid of this}
-
+We are now ready to verify the last precondition of \cref{thm:premodelIsModel}.
 
+\begin{proposition}
+	Fibrant universes imply the fibrant extension property.
+\end{proposition}
+\begin{proof}
+	Let \(f : A → X\) be a fibration and \(m : X → Y\) be a cofibration. Let \(κ\) be large enough so that
+	\(f\) is \(κ\)-small. We can classify \(f\) by a map \(a : X → \U\) and get the following diagram in the base.
+	\begin{eqcd*}
+		X \arrow[r,"a"] \arrow[d,"m"] & \U \arrow[d] \\
+		X' \arrow[r] \arrow[ru, dashed,"a'"] & *
+	\end{eqcd*}
+	As \U is fibrant this gives us a lift \(a'\). We can then get the required fibration by pulling
+	back \(π_κ\) along \(a'\).
+	\begin{eqcd*}
+			A
+				\arrow[rr]
+				\arrow[dr,dashed]
+				\arrow[dd,"f"]
+			& & \dot{\mathcal{U}}_κ
+				\arrow[dd]
+		\\
+			{}
+			& |[alias=F]| Y'
+				\arrow[ur]
+			&
+		\\
+			X
+				\arrow[rr, "f_c" near start]
+				\arrow[rd,tail,"c"]
+			& & \mathcal{U}_κ
+		\\
+			{}
+			& |[alias=X]| Y
+				\arrow[ur,"a'"]
+			&
+		\arrow[from=F, to=X, crossing over, dashed]
+	\end{eqcd*}
+	Making the required diagram a pullback, by the double pullback lemma.
+\end{proof}
 
 \subsection{Dedekind Cubes}
 We will also need a description of the model structure on the Dedekind cubes. It is similar in construction, we just
@@ -703,7 +1007,7 @@ of \(A\) that agrees with the partial element, where it is defined. So giving an
 \end{equation}
 %
 It is an opration that given \([φ]\) and \(f\) returns an \(a\) and a wittness that the upper triangle commutes.
-The lower one commuts automatically by the virtue of \(a\) beeing a term of type \(A\). Notice that uniformity
+The lower one commuts automatically by the virtue of \(a\) being a term of type \(A\). Notice that uniformity
 does not appear explicitly in this description, but happens automatically as pullback squares are the
 interpretation of substitutions, and the type thoeretic rules around substitution already imply a uniform
 choice of our lifts.