\documentclass[../Main.tex]{subfiles}
\begin{document}

\section{Model structure}\label{modelStructure}

% TODO restructure lifting with respect to category
% awfs
% Then cubical sets

\subsection{Equivariant Cartesian Cubes}
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 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 quotient by swapping the dimensions of a square, the resulting space is not
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.

\begin{equation*}
\begin{tikzcd}[column sep=large, row sep=large]
* \arrow[r,"\id"] \arrow[d,tail,"f"] & *  \arrow[d,tail,"σf"'] \arrow[r] & * \arrow[d,tail] \arrow[r,"β"] & X \arrow[d,"f"] \\
\I^2 \arrow[r,"σ"', shift right=0.7ex] \arrow[r,"\id", shift left=0.7ex] \arrow[urrr, dashed, ,near end, "{j(αe,β)}"'] & \I^2 \arrow[urr, dashed, "{j(αeσ,β)}"] \arrow[r, "e"] & Q \arrow[r,"α"] & Y 
\end{tikzcd}
\end{equation*} % Fix twist of suboject

Here \(σ\) is the map that swaps the dimensions and  \(e\) is the coequalizer map. The hope would be, 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.
%

% \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 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 definition.
% 
% \begin{definition}\label{def:rightMaps}
% 	Let \J be category and \(J : \J → \M^→\) be a functor. Then an object \(f\) in
% 	\(\M^→\) is a \emph{right \(J\)-map} if for every object \(i\) in \J, and for every
% 	lifting problem
% 	\begin{equation*}
% 		\begin{tikzcd}[column sep=large,row sep=large]
% 			L \arrow[r,"α"] \arrow[d, "Ji"']  & X \arrow[d,"f"] \\
% 			M \arrow[r,"β"] \arrow[ur, dashed,"{j(α,β)}"] & Y
% 		\end{tikzcd}
% 	\end{equation*}
% 	there is a specified lift \(j(α,β)\), such that for every \((a,b) : k → i\) in \J, the diagram
%   \begin{equation*}
% 		\begin{tikzcd}[column sep=huge, row sep = large]
% 		  L' \arrow[r,"a"] \arrow[d,"Jk"'] & L \arrow[r,"α"] \arrow[d,"Ji"] & X \arrow[d,"f"] \\
% 		  M' \arrow[urr, dashed, near start, "{j(αa,βb)}"] \arrow[r,"b"] & M \arrow[ur, dashed, "{j(α,β)}"'] \arrow[r,"β"] & Y
% 		\end{tikzcd}
%   \end{equation*}
%   commutes.
% \end{definition}
% 
% \begin{remark}
% 	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 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
% \cite{bourkeAlgebraicWeakFactorisation2016,bourkeAlgebraicWeakFactorisation2016a}. The main takeaway for
% us is the following theorem \cite[][Theorem 2.28]{riehlAlgebraicModelStructures2011}
% 
% \begin{theorem}[Garner]\label{smallObject}
% 	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
% 		orthogonal factorization system on \(\M\), for some regular cardinal \(α_X\).
% 	\end{itemize}
% 	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 category satisfies \((\ast)\). And as \(\□\) is a presheaf
% 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
% the right lifting class.
% 
% Now we need to formulate our definitions in a way that agrees with this conditions of this theorem.
% 


\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 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 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
	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 arbitrary dimension, and
	as morphism Cartesian squares between those.
\end{definition}

\begin{definition}
	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}

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 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 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 sub-cube \(f : \I^n \rightarrowtail \I^k\),
we get a pullback square of the following form
\begin{equation*}
	\begin{tikzcd}
		\I^n \arrow[r,"\id"] \arrow[d,tail,"f"] \pb & \I^n \arrow[d,tail, "σf"] \\
		\I^k \arrow[r,"σ"] & \I^k
	\end{tikzcd}
\end{equation*}
whose right arrow we call \(σf\).
%
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 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*}
\begin{tikzcd}
	\left(\faktor{\□}{\I^k} \right) ^{→} × \left(\faktor{\□}{\I^k}\right)^{→} \arrow[r,"\hat{×}_{\I^k}"] & \left(\faktor{\□}{\I^k}\right)^→ \arrow[r,"\textrm{forget}"] & \□^→
\end{tikzcd}
\end{equation*}

What do we change by working in the slice?
For intuition let us first look at the case
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 being in the slice), this is the diagonal of the square. From
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
\end{align*}
But in the context of \(\I\), the answer is three.
\begin{align*}
	i:\I ⊢ 0 : \I && i:\I ⊢ 1 : \I && i:\I ⊢ i : \I
\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 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
this short note \cite{coquandVariationCubicalSets2014}, for a discussion see for example \cite{angiuliSyntaxModelsCartesian2021}.

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 definition we get.
\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}
			C \arrow[r,"c", tail] \arrow[dr] & \I^n \arrow[d,"ζ"] \arrow[dr,phantom, "\hat{×}_{\I^k}"] & \I^k \arrow[d,"\id"] \arrow[r,"{⟨\id,l⟩}"] & \I^k × \I^m \arrow[dl,"π_l"] \\
			  & \I^k & \I^k &
		\end{tikzcd}
	\end{equation*}
	is called \emph{generating trivial cofibration}, as a map in \(\□\) with signature \(B_{c,ζ,l} \rightarrowtail \I^m × \I^n\).
\end{definition}

\begin{figure}
	\centering
	\includesvg[inkscapearea=nocrop,inkscapedpi=500,width=15cm]{figures/trivial_cofibration.svg}
	\caption{An example construction of a trivial cofibration}
\end{figure}

We now want to define our fibrations as the uniform equivariant right lifting maps. To do this we need to define what this
actually means. Uniformity wants a choice of lifts that agree with pullback squares between (trivial) cofibrations. %TODO move the uniformity section upwards
\begin{equation*}
	\begin{tikzcd}[column sep=large]
		A \arrow[r, "a"] \arrow[d, tail] \arrow[dr, phantom, very near start, "\lrcorner"] & B \arrow[d, tail] \arrow[r,"x"] & X \arrow[d, two heads] \\
		\I^k \arrow[r,"b"] \arrow[rru, dashed, "{j(xa,yb)}"] & \I^n \arrow[r,"y"] \arrow[ru, dashed, "{j(x,y)}"'] & Y
	\end{tikzcd}
\end{equation*}
The uniformity condition wants that the triangle containing both chosen lifts commutes, or as an equation \(j(x,y)b = j(ax,yb)\).
We now need to combine the uniformity and the equivariance condition. As the pushout-product is functorial it is enough to
describe these conditions between the building blocks of our trivial cofibration and apply the pushout-product again.
Again we will do this in a slice and forget the slice afterwards.
\begin{equation*}
	\left(
	\begin{tikzcd}[column sep = normal]
		D \arrow[r,"a"] \arrow[d, tail, "∂"] \pb & C \arrow[d,tail,"c"] &[-20pt] \\
		\I^m \arrow[r,"α"] & \I^n \arrow[dr, "ζ"] & \\[-15pt]
		& & \I^k
	\end{tikzcd}
	\right)
	\hat{×}_{\I^k}
	\left(
	\begin{tikzcd}
		\I^k \arrow[d,"{⟨\id,l⟩}"] \arrow[r,"\id"] & \I^k \arrow[d,"{⟨\id,σl⟩}"] &[-30pt] \\
		\I^k × \I^l \arrow[r,"\id × σ"] & \I^k × \I^l \arrow[dr,"π_l"] & \\[-15pt]
		& & \I^k
	\end{tikzcd}
	\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 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}
	\begin{tikzcd}[column sep=large]
		B_{∂,ζα,l} \arrow[r,"{⟨α,a×σ⟩}"] \arrow[d, tail] & B_{c,ζ,σl} \arrow[d, tail] \\
		\I^m × \I^l \arrow[r, "α×σ"] & \I^n × \I^l
	\end{tikzcd}
\end{equation}
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
	generating cofibrations and as morphism squares of the shape defined in \cref{devilSquare}
	above.
\end{definition}
\begin{definition}
	A \emph{uniform equivariant fibration} is right map with respect to the inclusion functor of the category of generating
	uniform equivariant trivial cofibrations into \(\□^→\).
\end{definition}

\begin{notation}
	By \cref{awfs:smallObject} these categories of maps form an awfs. We call it \((\TCF,\FF)\) and the underlying wfs
	\((\Ct,\F)\)
\end{notation}

\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}

\begin{definition}[{\cites{bartonModel2CategoryEnriched2019}[def. 3.1.1]{cavalloRelativeEleganceCartesian2022}}]\label{def:preModelStructure}
	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}

\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
	\(f\):
	\begin{eqcd*}[row sep=large, column sep=large]
		Y \arrow[r,dashed] \arrow[d,"f"] \pb & Y' \arrow[d,dashed, "f'"]  \\
		X \arrow[r,"m"] & X'
	\end{eqcd*}
\end{definition}

\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}
		\item all objects are cofibrant;
		\item the fibration extension property is satisfied.
	\end{enumerate}
	Then the premodel structure on \(\M\) defines a model structure.
\end{theorem}

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 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}}]\label{thm:modelStructure:equivalenceExtension}
	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{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.

The general construction of these universes follow mostly the same idea. We lift a Grothendieck universe from \Set to
the desired presheaf category, obtaining a Hofmann-Streicher universe \cite{hofmannLiftingGrothendieckUniverses1997},
classifying small maps.
This works in general for any presheaf topos over a small site. Afterwards we restrict this universe to only small fibrations.
We are then faced with a challenge, we need to prove that the resulting classifier is itself a fibration. In some cases
this can be made easier or avoided by stating this construction in a specific way.

For example by the arguments in \cite[Section 7]{awodeyHofmannStreicherUniverses2023} it suffices to construct \emph{classifying types}.
\begin{definition}\label{def:modelStructure:classifyingType}
	A \emph{classifying type} for an awfs is a construction \(\Fib\) such that for every object \(X\)
	and every morphism \(f : A → X\) there is a map \({\Fib(f) : \Fib(A) → X}\) and the section are in correspondence with
	\(\mathrm{R}\)-algebra structures on \(f\).
	Given a map \(g : Y → X\) then \(\Fib\) is stable under
	pullbacks along \(g\).
	\begin{eqcd*}[row sep=large]
			g^*A
				\arrow[r]
				\arrow[d, "g^*f"']
				\pb
			& A
				\arrow[d, "f"]
		\\
			Y
				\arrow[r,"g"]
			& X
		\\
			\Fib(g^*A)
				\arrow[u, "\Fib(g^*f)"]
				\arrow[r]
				\arrow[ur,"\urcorner",phantom, very near start]
			& \Fib(A)
				\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 internalization
of the \(\R\)-algebra structures on \(f\).

We will first construct classifying types, after that we construct universes from it.

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 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,
\begin{eqcd}\label{diag:liftProbTerminal}
	A \arrow[d, tail] \arrow[r] & X \arrow[d] \\
	C \arrow[r] & *
\end{eqcd}
we might think of this as a filling porblem of some shape \(A\) in \(X\) to some shape \(C\) in \(X\).
Or in other words as a complition of a partial map\footnote{Recall that a partial map \(C → X\) is a span \(C \leftarrow A → X\),
where the left map is a monomorphism.} from \(C → X\). We can classify these these by the partial map classifier,
given by \(X^+ ≔ Σ_{φ:Ω}X^{[φ]}\)\todo{give a reference}. This is gives us an object \(X^+\) (technicaly equipped with a map into the terminal)
and a monomrphism \( η_X : X → X^+\) such that for evey partial map \(C → X\) there is a unique map \(a: C → X^+\) completing
the following pullback square.
\begin{eqcd*}
	A \arrow[d, tail] \arrow[r] \pb & X \arrow[d,"η_X"] \\
	C \arrow[r, "a"] & X^+
\end{eqcd*}
This makes \((−)^+\) into a pointed endofunctor, and with little surprise are the \(+\)-algebras in correspondence with
the \TFF-algebras.

\begin{proposition}[{\cite[Proposition 15]{awodeyCartesianCubicalModel2023}}]
	The algebras of the pointed endofunctor \((−)^+\) are in correspondence to the algebras of the pointed endofunctor \TFF
	with codomain \(*\).
\end{proposition}
\begin{proof}[Proofsketch:]
	A \(+\)-algebra is an object \(X\) together with a morphism \(α : X^+ → X\) such that \(α η_x = \id\).
	Take some lifting problem like \cref{diag:liftProbTerminal}, define the chosen map to be \(αa\). If we
	are given a chosen lift, we compose it with \(η_X\) to retrieve \(a\).
\end{proof}

The benefit of \((−)^+\)-algebras is, that they are morphisms in \□ rather than in \(\□^→\).
We can interalize the condition to be a \((−)^+\)-algebra by means of the internal \(\Hom\).
\begin{eqcd*}
		+\textrm{-Alg}(X)
			\arrow[d]
			\arrow[r]
			\pb
		& {[X^+,X]}
			\arrow[d,"{[η_X,\id_X]}"]
	\\
		*
			\arrow[r,"λ\id_X"]
		& {[X,X]}
\end{eqcd*}
It is immediatly clear that a sections of the left map correspond to the desired \(+\)-algebra structure.

If we want to archive the same with a trivial fibration that has arbitrary codomain \(Y\), we might just move
to the slice topos \(\faktor{\□}{Y}\), there such a map becomes again a map into the terminal.
To not be confused we will call the partial map classification functor in
the slice over \(Y\) by the name \((−)^{+Y}\). The algebras will be called relative \(+\)-algberas.
We have even more luck and this functor commutes with the pullback
functor \(\□ → \faktor{\□}{Y}\),
\begin{eqcd*}
		\faktor{\□}{Y}
			\arrow[r, "(−)^{+Y}"]
		& \faktor{\□}{Y}
	\\
		\□
			\arrow[u,"Y^*"]
			\arrow[r,"(−)^+"]
		& \□
			\arrow[u,"Y^*"]
\end{eqcd*}
which allows us to compute it fiberwise \cite[Proposition 12]{awodeyCartesianCubicalModel2023}. This allows us to write
\((A)^{+Y} = Σ_{y:Y}A_y^+\), where \(A_y\) is the fiber of \(A\) at \(y\). We will still continue to write \(+\)-Alg, when
there is no confusion.
As all the involved functors \((−)^+\), pullbacks and exponentials are pullback stable so is \(+\)-Alg. Wich lets us conlude
the following.
\begin{proposition}
	\(+\)-Alg is a classifying type for trivial cofibrations.
\end{proposition}


We will move down a very similar path as \cite{awodeyCartesianCubicalModel2023}, but need to keep track of the group
actions of the symmetric groups on representables.
For this we will pass to a category that \cite{solution} calls cubical species. The argument in essence will be very similar
to the argument there, though in a different language.

\begin{definition}[compare {\cite[Section 4]{solution}}]
	By abuse of notation we will say  \(Σ_k\) to be the one object groupoid induced by the symmetric group \(Σ_k\).
	Let \(Σ ≔ ∐_{k ∈ ℕ} Σ_k\), we define \(\□^Σ\) to be the category of \emph{cubical species}. For a cubical
	species \(A\) we write \(A_k\) for the cubical set in the image of \(Σ_k\).
\end{definition}
\begin{remark}
	\(\□^Σ\) is a presheaf topos.
\end{remark}
\begin{remark}
	\cite{solution} excludes the case for \(k = 0\), because they want to exhibit a model category on cubical species.
	For the construction on cubical Sets this makes no difference compare \cite[Remark 4.3.17]{solution}.
\end{remark}

We need to define our equivalent of an interval, and the generic point inclusion. Recall that a functor from a group
into a category is the same as choosing an object of that category together with a group action on it.
\begin{definition}[{\cite[Example 4.3.5]{solution}}]
	Let \(\mathrm{I} : Σ → \□\) be the functor that sends \(Σ_k\) to \(\I^k\) together with the group action that freely
	permutates the dimensions.
\end{definition}
\begin{remark}[{\cite[Lemma 4.2.7]{solution}}]
	The interval \(\mathrm{I}\) is tiny.
\end{remark}

\begin{definition}[{\cite[Definition 4.3.3]{solution}}]
	The diagonal \(δ : \mathrm{I} → \mathrm{I} × \mathrm{I}\) as a map in the slice \(\faktor{\□^Σ}{\mathrm{I}}\) is called
	the generic point.
\end{definition}
\begin{remark}\label{rem:modelStructure:cubicalSpeciesPremodelStructure}
	Our classifcation induce a premodle structure on cubical species, where the cofibrations are all monomorhpisms,
	the trivial fibrations are classified by relative \(+\)-algebras and the fibrations are those maps such that their pullback
	to the slice over \(\mathrm{I}\) are getting send
	to a trivial fibration by \(δ ⇒ (−)\). Premodel structures in this way are called \emph{generated by \(\mathrm{I}\)}.
\end{remark}
\begin{remark}\label{rem:modelStructure:speciesPremodelSrtucture}
	By general abstract nonesense the premodel structure from \cref{rem:modelStructure:cubicalSpeciesPremodelStructure} is
	an adjoint (because topoi are cartesian closed) cylindrical premodel structure.
\end{remark}
\begin{remark}\label{rem:modelStructure:cubicalSpeciesEquivalenceExtension}
	By \cref{thm:modelStructure:equivalenceExtension} this premodel structure also fulfills the equivalence extension
	property.
\end{remark}

We will need another property that again follows from general premodel structure theory. We will not get this
immediately for equivariant cubes, as these are not generated by an interval\footnote{we could infer
it from cubical species}. Namely that left maps are pullback
stable along right maps, for both factorization systems. 

\begin{theorem}[{\cites[§5]{awodeyCartesianCubicalModel2023}{hazratpour2categoricalProofFrobenius2024}[Proposition 3.4.2]{solution}}]
	Let \(E\) be a locally cartesian closed category with a premodel structure in which the cofibrations are the monomorphisms.
	Suppose there is an object \(I\) such that a map is a fibration just when the Leibniz exponential of its pullback
	to the slice over \(I\) by the diagonal \(δ : I → I × I\) is a trivial fibration in the slice premodel structure,
	then the premodel structure satisfies the Frobenius condition.
\end{theorem}


% We will classify what in \cite{awodeyCartesianCubicalModel2023} would be called biased fibrations with regard to \(δ_0\) in \(\□^Σ\).
% These are not the kind of fibrations we are interested in, as we want lifts against the generic point. We will sort that out later.
% As the monic maps in \(\□^Σ\) are precisely those that are componentwise monic, we are just going to characterize
% componentwise fibrations. But because we passed to \(\□^Σ\), the classifying type will have group actions on
% every level, and we need to restrict to those, that are invariant under those group actions.

The main idea to continue classifying uniform fibrations from here on out is quite simple. As being a uniform fibration is
equivalent by being send to a trivial fibration by the right adjoint of the leibniz applicationfunctor of the interval,
we get that a \(+\)-algebra structure on \(δ ⇒ f\)\todo{write the right thing here}
is equivalent to a \FF-algebra structure on \(f\). This must then
be reformulated, to get the desired map. This reformulation is quite tedious and so we will refer
for the details to
\cite[The classifying types of unbiased fibration structures]{awodeyCartesianCubicalModel2023}.
In the source this takes place in \□, but it only makes use of the features we already established for \(\□^Σ\).
An important detail
to this procedure is, that in order to get the resulting classifying type pullback stable, this argument uses that
the interval is tiny.

We get a pullback stable construction \(\Fib^Σ(f)\)\footnote{this can be made into a classifying type for some
awfs compare \cite[Section 4.]{solution}}\todo{this footnote 2 is bad, but how to make different}
whose sections now correspond componentwise to \FF-algebra structures, that are equivariant with respect
to the group action of \(Σ^k\).

We now going to extract the classifying type for equivariant cubical fibrations. For this we need to relate cubical sets
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 co-complete}
\(Γ\) compare \cite[Section 5.1]{solution}, which is given by

\begin{equation*}
	Γ(A) ≔ ∏\limits_{k∈ℕ}(A_k)^{Σ_k}
\end{equation*}

where \((A_k)^Σ_k\) is the cubical set of \(Σ_k\) fixed points. It is not hard to see that this is indeed
the right adjoint functor.

\begin{proposition}
	We have a pair of adjoints \(Δ ⊣ Γ\)
\end{proposition}
\begin{proof}
	We need to show
	\begin{equation*}
		\Hom_{\□^Σ}(Δ(A),B) = \Hom_{\□}\left(A,∏\limits_{k∈ℕ}(B_k)^{Σ_k}\right) \text{.}
	\end{equation*}
	But this is immediatly clear, on the right hand side we have componentwise equivariant natural translations
	from \(Δ(A)_k = A\) to \(B_k\). They can only be valued in the fixed points in \(B_k\) as \(Δ(A)_k\) carries the
	trivial group action. A map on the right side is also a collection of natural transformations from \(A\) to
	the fixed points of \(B_k\).
\end{proof}

We get now that an \FF-algebra on \(f : A → B\) structure corresponds to a section
\begin{eqcd*}
	{} & \mathrm{Fib}^{Σ_k}(Δ(A))
		\arrow[d,"\mathrm{Fib}^{Σ_k}(Δ(f))"]
	\\ Δ(B) \arrow[r,equal]
		\arrow[ru, dashed]
	& Δ(B)
\end{eqcd*}
By adjointness we can transpose this lift to a lift in cubical sets, and by pulling back
along the adjunction unit to splits of a map over \(B\) (compare \cite[Lemma 5.3.3,2.1.16]{solution}).
\begin{eqcd*}[row sep=large]
	\mathrm{Fib}(B)
		\arrow[d,"\mathrm{Fib}(f)"]
		\arrow[r]
		\pb
	& Γ(\mathrm{Fib}^{Σ_k}(Δ(A)))
		\arrow[d,"Γ(\mathrm{Fib}^{Σ_k}(Δ(f)))"]
	\\ B \arrow[r,"η_B"]
		\arrow[ru, dashed]
		\arrow[u,bend left, dashed]
	& ΓΔ(B)
\end{eqcd*}

\begin{remark}
	From this discussion it is also clear that \(f\) is a fibration in \□, if and only if \(Δ(f)\) is
	a fibration in \(\□^Σ\).
\end{remark}

We will now present the idea, how to get fibrant universes from such classifying types.
This is mainly taken from \cite[Section 7]{awodeyHofmannStreicherUniverses2023}.
One might hope that we can construct a universal fibration, in the sense that every fibration
is a pullback of this universal fibration. This can not happen for size reasons. We will do
the next best thing and construct a universe for big enough kardinals \(κ\). Because
our set theory has Grothendieck universes this will give us universes for \(κ\) small fibrations.

To start we will call our Hofmann-Streicher, or \(κ\)-small map classifier, \({p : \dot{\mathcal{V}}_κ  → \mathcal{V}_κ}\).

\begin{theorem}[{\cite[Proposition 10]{awodeyHofmannStreicherUniverses2023}}]
	For a large enough \(κ\), there is a universe for \(κ\)-small fibrant maps, in the sense that there is
	a small fibration \(π : \dot{\mathcal{U}}_κ → \mathcal{U}_κ\) such that every small fibration \(f : A → X\), is
	a pullback of it along a connonical classifying map \(a\)
	\begin{eqcd*}
		A
			\pb
			\arrow[d,"f"]
			\arrow[r]
		& \dot{\mathcal{U}}_{κ}
			\arrow[d,"π_κ"]
	\\
		\mathcal{X}
			\arrow[r,"a"]
		& \mathcal{U}
	\end{eqcd*}
\end{theorem}

\begin{proof}
We can then construct our universe that classifies \(κ\)-small fibrations by setting \(\mathcal{U}_κ ≔ \mathrm{Fib}(\dot{\mathcal{V}}_κ)\)
and building the following pullback.
\begin{eqcd*}[row sep=large, column sep = large]
		\dot{\mathcal{U}}_κ
			\pb
			\arrow[d,"π_κ"]
			\arrow[r]
		& \dot{\mathcal{V}}_{κ}
			\arrow[d,"p"]
	\\
		\mathcal{U}
			\arrow[r,"\mathrm{Fib}(p)"]
		& \mathcal{V}
\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*}[]
		\dot{\mathcal{U}}_κ
			\pb
			\arrow[d,"π_κ"]
			\arrow[r]
		& \dot{\mathcal{V}}_{κ}
			\arrow[d,"p"]
	\\
		\mathcal{U_κ}
			\arrow[r,"\mathrm{Fib}(p)"]
		& \mathcal{V_κ}
	\\
		\mathrm{Fib}(\dot{\mathcal{U}}_κ)
			\arrow[u]
			\arrow[r]
			\arrow[ur,phantom,very near start,"\urcorner"]
		& \mathrm{Fib}(\dot{\mathcal{V}}_κ)
			\arrow[u,"\mathrm{Fib}(p)"]
\end{eqcd*}
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*}[row sep=small, column sep=small]
		{}
		& {}
		& \dot{\mathcal{U_κ}}
			\arrow[dr]
			\arrow[dd]
		&
	\\
		{}
		& |[alias=A]| A
			\arrow[rr,crossing over]
			\arrow[ru,dashed]
		& & \dot{\mathcal{V}_κ}
			\arrow[dd]
	\\
		\Fib(A)
			\arrow[rr]
			\arrow[dr]
		& & \mathcal{U_κ}
			\arrow[dr]
		&
	\\
		{}
		& |[alias=X]| X
			\arrow[rr,"a"]
			\arrow[lu,dashed,"s",bend left]
			\arrow[ur,dashed,"s'"]
		& & \mathcal{V}
	\arrow[from=A,to=X,crossing over]
\end{eqcd*}
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}.

\begin{lemma}[{\cite[Proposition 26]{awodeyCartesianCubicalModel2023}}]
	A map \(f : Y → X\) is a fibration in \(\□^Σ\) if and only if the canonical map \(u\) to the pullback,
	in the following diagram, is a trivial fibration.
	\begin{eqcd*}
			Y^{\mathrm{I}} × \mathrm{I}
				\arrow[rrd,"\mathsf{ev}", bend left]
				\arrow[ddr,"f^{\mathrm{I}} × \id_\mathrm{I}"', bend right]
				\arrow[dr,dashed,"u"]
			& &
		\\
			{}
			& Y'
				\arrow[r]
				\arrow[d]
				\pb
			& Y
				\arrow[d,"f"]
		\\
			{}
			& X^{\mathrm{I}} × \mathrm{I}
				\arrow[r,"\mathsf{ev}"']
			& X
	\end{eqcd*}
\end{lemma}
\begin{proof}
	\todo{in leibniz chapter introduce \(δ ⇒ f\) in the slice}
	Let us write out \(δ ⇒ f\).
	\[δ ⇒ f = ⟨f^\mathrm{I} × \id_\mathrm{I}, ⟨\mathsf{ev}, p_2⟩⟩: Y^\mathrm{I} × \mathrm{I} → (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\]
	We interpolate the above pullback square with another one.
	\begin{eqcd*}
			Y'
				\arrow[r]
				\arrow[d]
				\pb
			& Y × \mathrm{I}
				\arrow[d]
				\arrow[r]
				\pb
			& Y
				\arrow[d,"f"]
		\\
			X^{\mathrm{I}} × \mathrm{I}
				\arrow[r,"{⟨\mathsf{ev},\id_\mathrm{I}⟩}"']
			& X × \mathrm{I}
				\arrow[r,"p_1"']
			& X
	\end{eqcd*}
	By the double pullback lemma the outer square is also a pullback and thus
	\(Y' \simeq (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\) and \(δ ⇒ f \simeq u\).
\end{proof}
\begin{corollary}[{\cite[Corollary 27]{awodeyCartesianCubicalModel2023}}]\label{cor:27}
	An \(X\) in \(\□^Σ\) is fibrant if and only if the canonical map \(u\) to the pullback, in the following diagram
	is a trivial fibration.
	\begin{eqcd*}
			X^{\mathrm{I}} × \mathrm{I}
				\arrow[rrd,"\mathsf{ev}", bend left]
				\arrow[ddr,"p_2"', bend right]
				\arrow[dr,dashed,"u"]
			& &
		\\
			{}
			& \mathrm{I} × X
				\arrow[r]
				\arrow[d]
				\pb
			& X
				\arrow[d]
		\\
			{}
			& \mathrm{I}
				\arrow[r]
			& *
	\end{eqcd*}
\end{corollary}
\begin{proof}
	This is a special case of the lemma above.
\end{proof}
\begin{theorem}[{\cites[Proposition 120]{awodeyCartesianCubicalModel2023}[compare][Proposition 5.3.9]{solution}}]
	The base of the universe \U is a fibrant object.
\end{theorem}
\begin{proof}
	By \cref{cor:27} it suffices to check that the map \(u = ⟨p_2,\mathsf{ev}⟩\) in the following diagram in \(\□^Σ\),
	is a trivial fibration.
	\begin{eqcd*}
			Δ(\U)^{\mathrm{I}} × \mathrm{I}
				\arrow[rrd,"\mathsf{ev}", bend left]
				\arrow[ddr,"p_2"', bend right]
				\arrow[dr,dashed,"u"]
			& &
		\\
			{}
			& \mathrm{I} × Δ(\U)
				\arrow[r]
				\arrow[d]
				\pb
			& Δ(\U)
				\arrow[d]
		\\
			{}
			& \mathrm{I}
				\arrow[r]
			& *
	\end{eqcd*}
	To show this we consider the following lifting problem:
	\begin{eqcd*}
			C
				\arrow[r,"{⟨a',ic⟩}"]
				\arrow[d,tail,"c"]
			& Δ(\U)^\mathrm{I} × \mathrm{I}
				\arrow[d,"{⟨p_2,\mathsf{ev}⟩}"]
		\\
			Z
				\arrow[r,"{⟨i,b⟩}"]
				\arrow[ur,dotted]
			& \mathrm{I} × Δ(\U)
	\end{eqcd*}
	Transposing this problem along the exponential product adjunction we get:
	\begin{eqcd}\label{eq:modelStructure:mapEq}
			C
				\arrow[r,"{⟨\id_C,ic⟩}"]
				\arrow[d,"c",tail]
			& C × \mathrm{I}
				\arrow[d,"c × \id_I"]
				\arrow[ddr,"a", bend left]
			&
		\\
			Z
				\arrow[r,"{⟨\id_i,i⟩}"]
				\arrow[rrd,"b",bend right]
			& Z × \mathrm{I}
				\arrow[dr,dotted]
			&
		\\
			{}
			& & Δ(\U)
	\end{eqcd}
	where \(a\) is the uncurried versien of \(a'\). We would get such a desired map, if this was a pushout
	diagram via the coparing \([a,b]\). So let us compare \(Z × \mathrm{I}\) with the pushout.
	\begin{eqcd*}
			C
				\arrow[r,"{⟨\id_C,ic⟩}"]
				\arrow[d,"c",tail]
			& C × \mathrm{I}
				\arrow[d,"c × \id_\mathrm{I}"]
				\arrow[ddr,"c×\id_\mathrm{I}", bend left]
			&
		\\
			Z
				\arrow[r,]
				\arrow[rrd,"{⟨id_Z,i⟩}",bend right]
			& Z +_C (C × \mathrm{I})
				\arrow[dr,dotted,"d"]
			&
		\\
			{}
			& & Z × \mathrm{I}
	\end{eqcd*}
	This is exactly the definition of pushout product so we have \(d = c \× δ\), which is a trivial cofibration.
	And as \(\□^Σ\) has the equivalence extension property \cref{rem:modelStructure:cubicalSpeciesEquivalenceExtension},
	we can extend \([a,b]\) to the desired map in \cref{eq:modelStructure:mapEq}, and with this we get our desired lift.
\end{proof}

\todo{show fibrancy, this is hard and long, but needed for the next part. Or admit defeat and write something here}
\todo{get names for projections consistent}

\todo{introduce Leibniz pullback exponential}
\todo{introduced (unbiased) uniform fibrations and how they behave with leibniz constructions}
\todo{hate my life}

\subsubsection{From Premodel Structure to Model Structure}
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
don't need explicit equivariance. It turns out that in the presence of connections we get equivariance for free
\cite[Remark 4.2.26]{cavalloRelativeEleganceCartesian2022}. While the argument that this modelstructure indeed is a
model structure constructing univalent universes is somewhat easier, as we can extract it from an internal description
in the presheaf topos, by using strategies from \cite{LOPS}. As we only need this model structure for a later argument
we will not present all the arguments here.

Characterizing cofibrations and trivial fibrations will done as above.

\begin{definition}
	A \emph{generating cofibration} is a monomorphism into a cube \(c : C ↣  \I^n\)
\end{definition}

\begin{definition}
	A \emph{uniform trivial fibration} is a map with the uniform right lifting property against the generating cofibrations
\end{definition}

It will be usefull for our later development, to give a characterization in the internal language of the presheaf topos
\(\□_{∧∨}\). For more details on the interpretation of the internal semantics of cubical sets see \cite{awodeyKripkeJoyalForcingType2021}.
For the this style of modeling cubical type thoery inside of topoi see \cite{ortonAxiomsModellingCubical2018}. 
We will first give the characterization, then try to give some intuition why it makes sense and afterwards give a prove.


\begin{equation}\label{eq:TFib}
	\TFib A ≔ Π_{φ:Ω}Π_{f:[φ] → A} Σ_{a:A} Π_{α: [φ]} v(α) = a
\end{equation}

\missingfigure{draw a tfib explanation}

So assume we have a type \(A\) in some context \(Γ\). For the discussion we will identify types with their
respecting display maps, to keep the notational overhead low.
In this context the display map of \([φ]\) is monomorphism into \(Γ\), or
in other words a subterminal in \(\faktor{\□}{Γ}\). The term \(f : [φ] → A\) corresponds to a map from \([φ]\)
to \(A\). As this is a subterminal we could view it as a partial element of \(A\), or under the analogy to spaces we can
think of \(A\)
like a bundle over \(Γ\), we specify an element in only some fibers of \(A\). The \(a\) now corresponds to a full element
of \(A\) that agrees with the partial element, where it is defined. So giving an element of the type
\(\TFib A\) is like giving an operation that can fill partial elements. Or formulated as a lifting problem:
\begin{equation}
	\begin{tikzcd}
		{[φ]} \arrow[r,"f"] \arrow[d,tail]  & A \arrow[d] \\
		Γ \arrow[r,"\id"] \arrow[ru,dashed,"a"'] & Γ
	\end{tikzcd}
\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\) 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.

\todo{give a proof or get rid of the claim that we do}

We can also give an anolog description of fibrations. As we do not need to think about equivariance the descriptions
gets a bit less involved but stays basically the same.

\begin{definition}
	Let \(c : C ↣ \I^n\) be monic a \emph{generating trivial cofibration} is a map of the form
	\( c \× δ_k\)
\end{definition}

\begin{definition}
	A \emph{uniform fibration} is a uniform right lifting map against generating trivial cofibrations.
\end{definition}

\begin{proposition}[{\cite[Remark 4.2.26]{cavalloRelativeEleganceCartesian2022}}]\label{prop:dedekindEquivariant}
	The uniform fibrations of \(□_{∧∨}\) are equivariant.
\end{proposition}




% % \subsubsubsection{Internal description}
% For our further development we also want an internal description of our fibrations. This turns out to be more tricky then
% the trivial fibration variant for multiple reasons. The first is, that trivial cofibrations are harder to describe then
% cofibrations. We also have an additional condition namely equivariance.
% We also want a universe in the cubical type theory, that corresponds to a fibrant univers of fibrations in \(\□\). 
% 
% First we need to discuss, how type theory talks about lifting problems. 
% 
% We will do this the other way round. We first describe our fibrant universe and then get the rest for free. We will
% do this in a way following \cite{LOPS}. The first important obesrvation will be that our functorial cylinder not only
% has a right adjoint, but an even further right adjoint. Or in other words our interval is tiny.
% This can be seen with ease, we can describe the cylinder path space adjunction by a functor on \(□\). Namely the
% product with \([1]\). One checks easaly that \(((−) × [1])_!\) is isomporhic to the product with \(\I\) in \(\□\).
% Like in any presheaf topos we get an induced adjoint triple. This situation is very common to variants of cubical
% sets. In contrast to simplicial sets where this does not happen.
% \begin{equation}
	% ((−) × [1])_! ⊣ ((−) × [1])^* ⊣ ((−) × [1])_*
% \end{equation}
% \begin{proposition}
	% We have that
	% \begin{equation*}
		% (−)^\I \cong ((−) × [1])^*
	% \end{equation*}
% \end{proposition}
% \begin{proof}
	% Let \(A\) be a cubical Set. Because \(□\) is closed under products we get
	% by yoneda and the definition of exponentials the following natural isomorphism.
	% \begin{equation*}
		% A^\I_n \cong \□(\I^n,A^\I) \cong \□(\I^n × \I, A) \cong A([1]^n × [1]) = ((−) × [1])^*(A)_n
	% \end{equation*}
	% And thus an isomorphism between the given functors.
% \end{proof}
% 
% \begin{definition}
	% We write \(\sqrt{\phantom{−}} ­≔ ((−)×[1])_* \) for the rightmost adjoint of this adjunction
  % triple.
% \end{definition}

\end{document}
