das wird schon

src/Main.tex

@@ -5,7 +5,7 @@
 \Subject{see title}
 \Keywords{keyword}
 \end{filecontents*}
-\documentclass[DIV=calc,fontsize=12pt,draft=true,parskip]{scrartcl}
+\documentclass[DIV=calc,fontsize=12pt,draft=true]{scrartcl}
 \usepackage[a-2b,mathxmp]{pdfx}[2018/12/22]
 %\usepackage{pdfmanagement-testphase}
 %\DeclareDocumentMetadata{

src/Preliminaries/Leibniz_Construction.tex

@@ -5,17 +5,16 @@ We will see use a well know construction in homotopy theory, to
 elegantly construct a lot of interesting objects, the Leibniz construction.
 This section will mostly give a definition and some examples to get familiar with this construction.
 If the reader is already familiar with it, they might skip this section without any problems.
-
+We start by giving the definition.
-We start be giving the definition 
 \begin{definition}[Leibniz Construction]
 	Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) has finite pushouts. Let \(⊗ : \A × \B → \C \) be a bifunctor.
-	Then we define the \emph{Leibniz Construction} \(\hat{⊗} : \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
+	Then we define the \emph{Leibniz Construction} \(\⊗ : \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
 	that sends \(f : A → A' \) in \(\A\) and
-	\( g : B → B' \) in \(\B\), to \( f \hat{⊗}  g \) as defined as in the following diagram.
+	\( g : B → B' \) in \(\B\), to \( f \⊗  g \) as defined as in the following diagram.
 	\begin{equation*}
 	\begin{tikzcd}
 		A ⊗ B  \arrow[r, "f ⊗ \id"] \arrow[d, "\id ⊗ g"] \arrow[dr, phantom, "\ulcorner", very near end] & A' ⊗ \mathrlap{B} \phantom{A'} \arrow[ddr, bend left, "\id ⊗ g"] \arrow[d] & \\
-		\phantom{B'} \mathllap{A} ⊗ B' \arrow[drr, bend right, "f ⊗ \id"]  \arrow[r] & A ⊗ B' ∐\limits_{A ⊗ B} A' ⊗ B  \arrow[dr, dashed ,"f \hat{⊗} g"] & \\
+		\phantom{B'} \mathllap{A} ⊗ B' \arrow[drr, bend right, "f ⊗ \id"]  \arrow[r] & A ⊗ B' ∐\limits_{A ⊗ B} A' ⊗ B  \arrow[dr, dashed ,"f \⊗ g"] & \\
 		& & A' ⊗ B'
 	\end{tikzcd}
 	\end{equation*}
@@ -28,10 +27,10 @@ familiar with them.
 
 \begin{example}\label{ex:leib:prism}
 	Let \(δ_k : * → Δ^1\) for \(k ∈ {0,1}\) be one of the endpoint inclusions into the interval and \(i : \∂ Δ^n → Δ^n\) the boundary
-	inclusion of the \(n\)-simplex, then \(δ_k \hat{×} i\) is the inclusion of a prism without its interior and one cap, into the prism.
+	inclusion of the \(n\)-simplex, then \(δ_k \× i\) is the inclusion of a prism without its interior and one cap, into the prism.
 \end{example}
-This gives us a description of a possible set of generating trivial cofibrations. This will be an ongoing theme. For cubical sets we
+This gives us a description of a possible set of generating trivial cofibrations. This will be an ongoing theme.
-will define trivial cofibrations in this fashion. We can even observe something stronger. If we would replace the boundary inclusion
+We can even observe something stronger. If we would replace the boundary inclusion
 of the \(n\)-simplex with the boundary inclusion of an arbitrary space \(X\). We get the inclusion of the cylinder object of \(X\)
 without a cap and its interior into the cylinder.
 \begin{figure}
@@ -40,13 +39,14 @@ without a cap and its interior into the cylinder.
 \end{figure}
 
 \begin{observation}
-	If \(f\) and \(g\) are cofibrations then \(f \hat{×} g\) is too. If one of them is a trivial cofibration then so is \(f \hat{×} g\).
+	If \(f\) and \(g\) are cofibrations then \(f \× g\) is too. If one of them is a trivial cofibration then so is \(f \× g\).
 \end{observation}
-This has far reaching consequences, and one can define a monoidal model category where this are one of the axioms
+This has far reaching consequences, and one can define the notion of a  monoidal model category where this are one of the axioms
-for the tensor functor. For more
+for the tensor functor. This axioms basically states that the tensor product behaves homotopicaly. For more
 detail see \cite{hoveyModelCategories2007}. We are not going to need much of this theory explicitly. But it is worthy to note
 that all examples of model categories that we are going to encouter are of this form.
 
+
 We will also encouter the basically same construction as \cref{ex:leib:prism} in another way. We can also get the Cylinder object
 functorialy in \Δ, such that the cap inclusions are natural transformations.
 We can also get the inclusion the Leibniz product produces in a natural  manner via the Leibniz application.
@@ -57,22 +57,84 @@ We can also get the inclusion the Leibniz product produces in a natural  manner
 	product with the interval).
 	Let be one of the inclusions \( δ_k : \Id → \I ⊗ (−) \), the natural transformation that embeds the space in one of the cylinder caps.
 	Let \( \∂ X → X \) be the boundery inclusion of \(X\).
-	Then \( δ_k \hat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
+	Then \( δ_k \widehat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
 \end{example}
 This kind of construction will later play an important role in the construction of our desired model categories.
+And as we will constructions like this more often we add a bit of notation for it.
+
+\begin{notation}
+	Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
+	be a nutral transformation. We write \(η \⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\).
+\end{notation}
+
+Here is a property that we will exploit fairly often.
+\begin{proposition}\label{rem:leibniz:adhesive}
+	Since every topos is adhesive \cite{lackAdhesiveQuasiadhesiveCategories2005}, the pushout-product and the
+	Leibniz application of \(A × (−)\), are stable under monomorhpisms in every topos.
+\end{proposition}
+
+The Leibniz construction has a dual construction, the Leibniz pullback construction
+\begin{definition}[Leibniz pullback Construction]
+	Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) has finite pullbacks. Let \(⊗ : \A × \B → \C \) be a bifunctor.
+	Then we define the \emph{Leibniz pullback construction} \(\widecheck{⊗ }: \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
+	that sends \(f : A → A' \) in \(\A\) and
+	\( g : B → B' \) in \(\B\), to \( f \widecheck{⊗}  g \) as defined as in the following diagram.
+	\begin{equation*}
+		\begin{tikzcd}
+			A ⊗ B
+				\arrow[rrd, "f ⊗ \id",bend left]
+				\arrow[ddr, "\id ⊗ g",bend right]
+				\arrow[rd, "", dashed]
+			& &
+		\\
+			{} & A ⊗ B' \displaystyle\prod_{A'⊗B'} A'⊗ B
+				\arrow[d]
+				\arrow[r]
+				\pb
+			& A' ⊗ \mathrlap{B} \phantom{A'}
+				\arrow[d, "\id ⊗ g"]
+		\\
+			{}
+			& \phantom{B'} \mathllap{A} ⊗ B'
+				\arrow[r, "f ⊗ \id"]
+			& A' ⊗ B'
+		\end{tikzcd}
+	\end{equation*}
+	If \(⊗\) is the exponential functor, we also call it the \emph{Leibniz pullback Hom}, \emph{pullback-power}, or \emph{pullback-hom}.
+	If \(⊗\) is the functor application functor we also call it the \emph{Leibniz pullback application}.
+\end{definition}
+Analog to the notation above we introduce the following notation
+\begin{notation}
+	Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
+	be a nutral transformation. We write \(η \widehat⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\).	As it is common in the literature we
+	also write for the special case \(A⊗ (−) = (−)^A\), the following \(η ⇒ (−) ≔ η \widecheck⊗ (−)\).
+\end{notation}
+
+Dualy to our observation above it will be a theme that the pullback-power sends fibrations to trivial fibrations.
+Or more formally:
+\begin{lemma}[{\cite[Lemma 4.10]{riehlTheoryPracticeReedy2014}}]
+	There is an adjunction \({η \× (−) ⊣ η ⇒ (−)}\), between the pushout-product and the pullback-power.
+\end{lemma}
+\begin{remark}
+	This holds in much more generality, for details see \cite[Lemma 2.1.15]{solution}
+\end{remark}
+\begin{remark}
+	Our main application of this lemma will be, that it gives us the ability to transpose lifting problems
+	between cofibrations and trivial fibrations, to lifting problems between trivial cofibrations and fibrations.
+\end{remark}
 
 We will also encouter another form of Leibniz application, which has at first glance not to do alot with homotopy. On
 the other hand one might read this as, getting the component of an natural transformation is some sort of a homotopic construction.
 \begin{lemma}
-	Let \(F,G : A → B \) and \(η : F ⇒ G\) be a natural transformation, and \A has in initial object \(∅\). Let
+	Let \(F,G : A → B \) and \(η : F ⇒ G\) be a natural transformation, and \A has an initial object \(∅\). Let
 	\(F\) and \(G\) preserve the initial object.
 	We write \(∅ → X\) for the unique map with the same type. Then we get \(η \at (∅ → X) = η_X\).
 \end{lemma}
-\begin{proof}\todo{this is contravariant and I'm too tired}
+\begin{proof}
 	We will draw the diagram from the definiton
 	\begin{eqcd*}
 		F (∅)  \arrow[r, "F(∅ → X)"] \arrow[d, "η_∅"] \arrow[dr, phantom, "\ulcorner", very near end] & F(X) \arrow[ddr, bend left, "η_X"] \arrow[d] & \\
-		G(∅) \arrow[drr, bend right, "G(∅ → X)"]  \arrow[r] & G(∅) ∐\limits_{F(∅)} \mathrlap{F(X)} \phantom{G(∅)} \arrow[dr, dashed ,"f \hat{⊗} g"] & \\
+		G(∅) \arrow[drr, bend right, "G(∅ → X)"']  \arrow[r] & G(∅) ∐\limits_{F(∅)} \mathrlap{F(X)} \phantom{G(∅)} \arrow[dr, dashed ,"η \widehat{@} (∅ → X)" description] & \\
 		& & G(X)
 	\end{eqcd*}
 	If we substitude \(F(\emptyset)\) and \(G(∅)\) with \(∅\) the claim directly follows.

src/Preliminaries/Model_Structure.tex

@@ -355,52 +355,52 @@ a trivial cofibration if set \(k = 0\) and \(m = 1\) in \cref{def:modelStructure
 
 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
+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
+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
+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.
+that the base of our constructed universe is fibrant.
-% In categorical terms it says the following.
+In categorical terms it says the following.
-% 
+
-% \begin{definition}[{\cite{sattlerEquivalenceExtensionProperty2017}}]
+\begin{definition}[{\cite{sattlerEquivalenceExtensionProperty2017}}]
-% 	A cylindrical premodel structure has the equivalence extension
+	A cylindrical premodel structure has the equivalence extension
-% 	property when any weak equivalence \(e\) over an object \(A\) can be extended along any cofibration
+	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:
+	\(i : A → B\) to a weak equivalence \(f\) over \(B\) with a specified codomain extending that of the original map:
-% 	\begin{eqcd*}
+	\begin{eqcd*}
-% 			X_0
+			X_0
-% 				\arrow[rr,dotted]
+				\arrow[rr,dotted]
-% 				\arrow[rd,"e"]
+				\arrow[rd,"e"]
-% 				\arrow[rdd,"p_0"']
+				\arrow[rdd,"p_0"']
-% 			& & Y_0
+			& & Y_0
-% 				\arrow[rd,dashed, "f"]
+				\arrow[rd,dashed, "f"]
-% 				\arrow[rdd,dotted]
+				\arrow[rdd,dotted]
-% 			&
+			&
-% 		\\
+		\\
-% 			{}
+			{}
-% 			& X_1
+			& X_1
-% 				\arrow[rr, crossing over]
+				\arrow[rr, crossing over]
-% 				\arrow[d,"p_1"]
+				\arrow[d,"p_1"]
-% 				\arrow[rrd,phantom,"\lrcorner" very near start]
+				\arrow[rrd,phantom,"\lrcorner" very near start]
-% 			& & Y_1
+			& & Y_1
-% 				\arrow[d,"q_1"]
+				\arrow[d,"q_1"]
-% 		\\
+		\\
-% 			{}
+			{}
-% 			& A
+			& A
-% 				\arrow[rr,"i"]
+				\arrow[rr,"i"]
-% 			& & B
+			& & B
-% 	\end{eqcd*}
+	\end{eqcd*}
-% 	In a setting such as a presheaf topos where we have universe levels,
+	In a setting such as a presheaf topos where we have universe levels,
-% 	there is an additional requirement: for sufficiently large inaccessible cardinals
+	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.
+	\(κ\), if \(p_0\), \(p_1\), and \(q_1\) are \(κ\)-small, so is the extended fibration.
-% \end{definition}
+\end{definition}
-% 
+
-% We could have equivalently used \cite[Proposition 5.1]{sattlerEquivalenceExtensionProperty2017},
+We could have equivalently used \cite[Proposition 5.1]{sattlerEquivalenceExtensionProperty2017},
-% but this version aligns more direct with the data that we are given.
+but this version aligns more direct with the data that we are given.
-% \begin{theorem}[{\cite[Theorem 3.3.3]{solution}}]
+\begin{theorem}[{\cite[Theorem 3.3.3]{solution}}]\label{thm:modelStructure:equivalenceExtension}
-% 	Let \(E\) be a locally Cartesian closed category with a cylindrical premodel
+	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
+	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\).
+	pushout-products in all slices. Then the equivalence extension property holds in \(E\).
-% \end{theorem}
+\end{theorem}
-% The pushout product claim is verified by \cref{TODO}\todo{adhesive note in Leibniz chapter}
+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.
@@ -541,12 +541,6 @@ to the argument there, though in a different language.
 	\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}
-\begin{remark}
-	Going forward we keep the names trivial fibrations,cofibrations, fibrationstructure, \dots, even though we don't
-	have defined any of this notions on \(\□^Σ\). We mean the objects that are equivalently classified in this
-	topos, like in the procedure above. This can actually be made into a modelstructure where these are the corresponding
-	fibrations, cofibrations, \dots, for details see \cite[Section 4]{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.
@@ -562,6 +556,33 @@ into a category is the same as choosing an object of that category together with
 	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.
@@ -570,7 +591,7 @@ into a category is the same as choosing an object of that category together with
 % 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 inteval,
+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
@@ -637,16 +658,21 @@ along the adjunction unit to splits of a map over \(B\) (compare \cite[Lemma 5.3
 	& ΓΔ(B)
 \end{eqcd*}
 
-We will now present the main idea, how to get fibrant universes from such classifying types.
+\begin{remark}
-The technical details can be found in \cite[Section 7]{awodeyHofmannStreicherUniverses2023}.
+	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 maps fibrations.
+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{proposition}[{\cite[Proposition 10]{awodeyHofmannStreicherUniverses2023}}]
+\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\)
@@ -662,7 +688,7 @@ To start we will call our Hofmann-Streicher, or \(κ\)-small map classifier, \({
 			\arrow[r,"a"]
 		& \mathcal{U}
 	\end{eqcd*}
-\end{proposition}
+\end{theorem}
 
 \begin{proof}
 We can then construct our universe that classifies \(κ\)-small fibrations by setting \(\mathcal{U}_κ ≔ \mathrm{Fib}(\dot{\mathcal{V}}_κ)\)
@@ -910,8 +936,171 @@ source material for the technical details.
 %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}
 
+\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}

src/resource.bib

@@ -1081,3 +1081,19 @@
   langid = {english},
   file = {/home/nerf/Zotero/storage/Y3K26BM6/Lack and Sobociński - 2005 - Adhesive and quasiadhesive categories.pdf}
 }
+
+@online{hazratpour2categoricalProofFrobenius2024,
+  title = {A 2-Categorical Proof of {{Frobenius}} for Fibrations Defined from a Generic Point},
+  author = {Hazratpour, Sina and Riehl, Emily},
+  date = {2024-02-22},
+  eprint = {2210.00078},
+  eprinttype = {arXiv},
+  eprintclass = {math},
+  doi = {10.48550/arXiv.2210.00078},
+  url = {http://arxiv.org/abs/2210.00078},
+  urldate = {2024-08-08},
+  abstract = {Consider a locally cartesian closed category with an object I and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of I defines a trivial fibration. Then the fibrations are also closed under pushforward.},
+  pubstate = {prepublished},
+  keywords = {18N45 18N40 03B38 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
+  file = {/home/nerf/Zotero/storage/ISNC6YKS/Hazratpour and Riehl - 2024 - A 2-categorical proof of Frobenius for fibrations .pdf;/home/nerf/Zotero/storage/BIR588ML/2210.html}
+}