From 9124739ccaa0c39ecc20f3d0d637ba267520d95b Mon Sep 17 00:00:00 2001 From: Dennis Frieberg Date: Thu, 8 Aug 2024 04:41:08 +0200 Subject: [PATCH] tired and scared --- src/Main.tex | 10 +- src/Preliminaries/Model_Structure.tex | 444 +++++-- src/resource.bib | 1570 +++++++++++++------------ 3 files changed, 1174 insertions(+), 850 deletions(-) diff --git a/src/Main.tex b/src/Main.tex index dd4b556..e33e15c 100644 --- a/src/Main.tex +++ b/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{\hat{×}}} -\newcommand*{\at}{\mathbin{\hat{@}}} +\newcommand*{\⊗}{\mathbin{\widehat{⊗}}} +\newcommand*{\×}{\mathbin{\widehat{×}}} +\newcommand*{\at}{\mathbin{\widehat{@}}} \newcommand*{\□}{\ensuremath{\widehat{□}}\xspace} \newcommand*{\Δ}{\ensuremath{\widehat{Δ}}\xspace} \newcommand*{\dCube}{\ensuremath{□_{∧∨}}\xspace} diff --git a/src/Preliminaries/Model_Structure.tex b/src/Preliminaries/Model_Structure.tex index 20d9f6e..25cd9e3 100644 --- a/src/Preliminaries/Model_Structure.tex +++ b/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 -contractable, while in spaces it is. The idea is to correct this defect, by making the embedding +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. @@ -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 -the coequilizer, would now present a lift for the right most lifting problem. But in general that +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. % @@ -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 -% category over a countable category, it is locally presentable. Also by beeing a presheaf category makes it automatically cocomplete. +% 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 @@ -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 - as morphism cartesian squares between those. + 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 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 -with a one dimensional context. The point in in this context ist the terminal object in \(\faktor{\□}{\I}\). +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 beeing 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 +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 @@ -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. -\begin{definition} +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} @@ -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 second condition we won't show directly. We will get for free if we construct fibrant universes, which we want to do anyway. +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}}] +% 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 -of the \(\R\)-algbera structures on \(f\). +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 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} -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} - +\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 @@ -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. diff --git a/src/resource.bib b/src/resource.bib index 8d1df5a..2952fcc 100644 --- a/src/resource.bib +++ b/src/resource.bib @@ -1,135 +1,29 @@ -@article{ABCHFL, - title = {Syntax and Models of {{Cartesian}} Cubical Type Theory}, - author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Harper, Robert and Hou (Favonia), Kuen-Bang and Licata, Daniel R.}, - date = {2021-04}, - journaltitle = {Mathematical Structures in Computer Science}, - volume = {31}, - number = {4}, - pages = {424--468}, - publisher = {Cambridge University Press}, - issn = {0960-1295, 1469-8072}, - doi = {10.1017/S0960129521000347}, - url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/syntax-and-models-of-cartesian-cubical-type-theory/01B9E98DF997F0861E4BA13A34B72A7D}, - urldate = {2023-04-21}, - abstract = {We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.}, - langid = {english}, - keywords = {ABCHFL,cubical type theory,homotopy type theory,Type theory}, - file = {/home/nerf/Zotero/storage/2MPEKIEC/Angiuli et al. - 2021 - Syntax and models of Cartesian cubical type theory.pdf} -} - -@inproceedings{angiuliCartesianCubicalComputational2018, - title = {Cartesian {{Cubical Computational Type Theory}}: {{Constructive Reasoning}} with {{Paths}} and {{Equalities}}}, - shorttitle = {Cartesian {{Cubical Computational Type Theory}}}, - booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{CSL}}.2018.6}, - author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert}, - date = {2018}, - publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik}, - doi = {10.4230/LIPIcs.CSL.2018.6}, - url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6}, - urldate = {2024-04-28}, - abstract = {We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.}, - eventtitle = {27th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2018)}, - langid = {english}, - file = {/home/nerf/Zotero/storage/XTZNK2WW/Angiuli et al. - 2018 - Cartesian Cubical Computational Type Theory Const.pdf} -} - -@online{awodeyCartesianCubicalModel2023, - title = {Cartesian Cubical Model Categories}, - author = {Awodey, Steve}, - date = {2023-07-14}, - eprint = {2305.00893}, +@unpublished{coquandConstructiveSheafModels2020, + title = {Constructive Sheaf Models of Type Theory}, + author = {Coquand, Thierry and Ruch, Fabian and Sattler, Christian}, + date = {2020-07-08}, + eprint = {1912.10407}, eprinttype = {arXiv}, eprintclass = {math}, - doi = {10.48550/arXiv.2305.00893}, - url = {http://arxiv.org/abs/2305.00893}, - urldate = {2024-08-03}, - abstract = {The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.}, - pubstate = {prepublished}, - keywords = {18N40 18B25 18N45,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/KWCXVX7B/Awodey - 2023 - Cartesian cubical model categories.pdf;/home/nerf/Zotero/storage/PNTHDEYX/2305.html} + url = {http://arxiv.org/abs/1912.10407}, + urldate = {2022-04-25}, + abstract = {We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.}, + keywords = {Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/BM86P38T/Coquand et al. - 2020 - Constructive sheaf models of type theory.pdf;/home/nerf/Zotero/storage/VIMEBY7W/1912.html} } -@book{awodeyCategoryTheory2006, - title = {Category {{Theory}}}, - author = {Awodey, Steve}, - date = {2006-05-25}, - publisher = {Oxford University Press}, - doi = {10.1093/acprof:oso/9780198568612.001.0001}, - url = {https://doi.org/10.1093/acprof:oso/9780198568612.001.0001}, - urldate = {2023-09-12}, - abstract = {This book is a text and reference book on Category Theory, a branch of abstract algebra. The book contains clear definitions of the essential concepts, which are illuminated with numerous accessible examples. It provides full proofs of all the important propositions and theorems, and aims to make the basic ideas, theorems, and methods of Category Theory understandable. Although it assumes few mathematical pre-requisites, the standard of mathematical rigour is not compromised. The material covered includes the standard core of categories; functors; natural transformations; equivalence; limits and colimits; functor categories; representables; Yoneda's lemma; adjoints; and monads. An extra topic of cartesian closed categories and the lambda-calculus is also provided.}, - isbn = {978-0-19-856861-2} -} - -@online{awodeyHofmannStreicherUniverses2023, - title = {On {{Hofmann-Streicher}} Universes}, - author = {Awodey, Steve}, - date = {2023-07-11}, - eprint = {2205.10917}, +@unpublished{gambinoEffectiveModelStructure2021, + title = {The Effective Model Structure and \$\textbackslash infty\$-Groupoid Objects}, + author = {Gambino, Nicola and Henry, Simon and Sattler, Christian and Szumiło, Karol}, + date = {2021-03-10}, + eprint = {2102.06146}, eprinttype = {arXiv}, eprintclass = {math}, - doi = {10.48550/arXiv.2205.10917}, - url = {http://arxiv.org/abs/2205.10917}, - urldate = {2024-07-05}, - abstract = {We have another look at the construction by Hofmann and Streicher of a universe \$(U,\{\textbackslash mathsf\{E\}l\})\$ for the interpretation of Martin-L\textbackslash "of type theory in a presheaf category \$\textbackslash psh\{\textbackslash C\}\$. It turns out that \$(U,\{\textbackslash mathsf\{E\}l\})\$ can be described as the \textbackslash emph\{categorical nerve\} of the classifier \$\textbackslash dot\{\textbackslash Set\}\textasciicircum\{\textbackslash mathsf\{op\}\} \textbackslash to \textbackslash op\{\textbackslash Set\}\$ for discrete fibrations in \$\textbackslash Cat\$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf \$P : \textbackslash op\{\textbackslash C\}\textbackslash to\textbackslash Set\$ to its category of elements \$\textbackslash int\_\textbackslash C P\$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.}, - pubstate = {prepublished}, - keywords = {Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/NIIL8ZAK/Awodey - 2023 - On Hofmann-Streicher universes.pdf;/home/nerf/Zotero/storage/J3DQ66DM/2205.html} -} - -@online{awodeyKripkeJoyalForcingType2021, - title = {Kripke-{{Joyal}} Forcing for Type Theory and Uniform Fibrations}, - author = {Awodey, S. and Gambino, N. and Hazratpour, S.}, - date = {2021-10-27}, - eprint = {2110.14576}, - eprinttype = {arXiv}, - eprintclass = {math}, - doi = {10.48550/arXiv.2110.14576}, - url = {http://arxiv.org/abs/2110.14576}, - urldate = {2024-02-21}, - abstract = {We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.}, - pubstate = {prepublished}, - keywords = {03G30 03B38 18F20 18N45,Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/NNQITW4X/Awodey et al. - 2021 - Kripke-Joyal forcing for type theory and uniform f.pdf;/home/nerf/Zotero/storage/M3MTFM97/2110.html} -} - -@article{awodeyQuillenModelStructures, - title = {Quillen Model Structures on Cubical Sets}, - author = {Awodey, Steve}, - pages = {31}, - langid = {english}, - file = {/home/nerf/Zotero/storage/79HSXCBI/Awodey - Quillen model structures on cubical sets.pdf} -} - -@incollection{balchinBisimplicialSets2021, - title = {Bisimplicial {{Sets}}}, - booktitle = {A {{Handbook}} of {{Model Categories}}}, - author = {Balchin, Scott}, - editor = {Balchin, Scott}, - date = {2021}, - pages = {205--215}, - publisher = {Springer International Publishing}, - location = {Cham}, - doi = {10.1007/978-3-030-75035-0_12}, - url = {https://doi.org/10.1007/978-3-030-75035-0_12}, - urldate = {2024-04-10}, - abstract = {The category of bisimplicial sets is the functor category \$\$\textbackslash mathbf\{Set\} \textasciicircum\{(\textbackslash varDelta \textasciicircum\{op\} \textbackslash times \textbackslash varDelta \textasciicircum\{op\})\}\$\$Set(Δop×Δop), which we denote \$\$\textbackslash mathbf\{ssSet\} \$\$ssSet. Equivalently, \$\$\textbackslash mathbf\{ssSet\} \$\$ssSetis the category of simplicial objects in simplicial sets, i.e., \$\$\textbackslash mathbf\{ssSet\} \textbackslash cong \textbackslash mathbf\{sSet\} \textasciicircum\{\textbackslash varDelta \textasciicircum\{op\}\}\$\$ssSet≅sSetΔop. Under this identification, one could equally call a bisimplicial set a simplicial space.}, - isbn = {978-3-030-75035-0}, - langid = {english}, - file = {/home/nerf/Zotero/storage/3LJ3IU2J/Balchin - 2021 - Bisimplicial Sets.pdf} -} - -@article{bartonModel2CategoryEnriched2019, - title = {A {{Model}} 2-{{Category}} of {{Enriched Combinatorial Premodel Categories}}}, - author = {Barton, Reid William}, - date = {2019-09-10}, - issn = {4201-3127}, - url = {https://dash.harvard.edu/handle/1/42013127}, - urldate = {2024-04-28}, - abstract = {Quillen equivalences induce equivalences of homotopy theories and therefore form a natural choice for the "weak equivalences" between model categories. In [21], Hovey asked whether the 2-category Mod of model categories has a "model 2-category structure" with these weak equivalences. We give an example showing that Mod does not have pullbacks, so cannot be a model 2-category. We can try to repair this lack of limits by generalizing the notion of model category. The lack of limits in Mod is due to the two-out-of-three axiom, so we define a premodel category to be a complete and cocomplete category equipped with two nested weak factorization systems. Combinatorial premodel categories form a 2-category CPM with excellent algebraic properties: CPM has all limits and colimits and is equipped with a tensor product (representing Quillen bifunctors) which is adjoint to an internal Hom. The homotopy theory of a model category depends in an essential way on the weak equivalences, so it does not extend directly to premodel categories. We build a substitute homotopy theory under an additional axiom on the premodel category, which holds automatically for a premodel category enriched in a monoidal model category V. The 2-category of combinatorial V-premodel categories VCPM is simply the 2-category of modules over the monoid object V, so VCPM inherits the algebraic structure of CPM. We construct a model 2-category structure on VCPM for V a tractable symmetric monoidal model category, by adapting Szumiło's construction of a fibration category of cofibration categories [35]. For set-theoretic reasons, constructing factorizations for this model 2-category structure requires a technical variant of the small object argument which relies on an analysis of the rank of combinatoriality of a premodel category.}, - langid = {english}, - annotation = {Accepted: 2019-12-11T10:06:35Z}, - file = {/home/nerf/Zotero/storage/ALJR3L7T/Barton - 2019 - A Model 2-Category of Enriched Combinatorial Premo.pdf} + url = {http://arxiv.org/abs/2102.06146}, + urldate = {2022-04-25}, + abstract = {For a category \$\textbackslash mathcal E\$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in \$\textbackslash mathcal E\$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated \$\textbackslash infty\$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when \$\textbackslash mathcal E\$ is, but is not a higher topos in general. We also characterise the \$\textbackslash infty\$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on \$\textbackslash mathcal E\$ spanned by Kan complexes in \$\textbackslash mathcal E\$, a result that suggests a close analogy with the theory of exact completions.}, + keywords = {18N40 (primary) 18N60 55U10,Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/QVGLME2U/Gambino et al. - 2021 - The effective model structure and $infty$-groupoi.pdf;/home/nerf/Zotero/storage/2YSZT8KA/2102.html} } @article{bergerExtensionNotionReedy2011, @@ -152,35 +46,38 @@ file = {/home/nerf/Zotero/storage/9CXJYQ22/Berger and Moerdijk - 2011 - On an extension of the notion of Reedy category.pdf;/home/nerf/Zotero/storage/E9DB6IW2/0809.html} } -@inproceedings{bezemModelTypeTheory2014, - title = {A {{Model}} of {{Type Theory}} in {{Cubical Sets}}}, - author = {Bezem, Marc and Coquand, Thierry and Huber, Simon}, - namea = {Herbstritt, Marc}, - nameatype = {collaborator}, - date = {2014}, - pages = {22 pages}, - publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany}, - doi = {10.4230/LIPICS.TYPES.2013.107}, - url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628/}, - urldate = {2023-08-28}, - abstract = {We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.}, - langid = {english}, - keywords = {000 Computer science knowledge general works,Computer Science}, - file = {/home/nerf/Zotero/storage/4KKXST7S/Bezem et al. - A model of type theory in cubical sets.pdf} +@article{garnerUnderstandingSmallObject2009, + title = {Understanding the Small Object Argument}, + author = {Garner, Richard}, + date = {2009-06}, + journaltitle = {Applied Categorical Structures}, + shortjournal = {Appl Categor Struct}, + volume = {17}, + number = {3}, + eprint = {0712.0724}, + eprinttype = {arXiv}, + pages = {247--285}, + issn = {0927-2852, 1572-9095}, + doi = {10.1007/s10485-008-9137-4}, + url = {http://arxiv.org/abs/0712.0724}, + urldate = {2022-04-26}, + abstract = {The small object argument is a transfinite construction which, starting from a set of maps in a category, generates a weak factorisation system on that category. As useful as it is, the small object argument has some problematic aspects: it possesses no universal property; it does not converge; and it does not seem to be related to other transfinite constructions occurring in categorical algebra. In this paper, we give an "algebraic" refinement of the small object argument, cast in terms of Grandis and Tholen's natural weak factorisation systems, which rectifies each of these three deficiencies.}, + keywords = {18A32 55U35,18C10,55U35,Algebraic model structures,Mathematics - Algebraic Topology,Mathematics - Category Theory,Small object argument,Weak factorisation system}, + file = {/home/nerf/Zotero/storage/7UVP29D5/Garner - 2009 - Understanding the Small Object Argument.pdf;/home/nerf/Zotero/storage/9V4MZU3G/Garner - 2009 - Understanding the small object argument.pdf;/home/nerf/Zotero/storage/8TPNVUAK/0712.html} } -@article{borceuxCauchyCompletionCategory1986, - title = {Cauchy completion in category theory}, - author = {Borceux, Francis and Dejean, Dominique}, - date = {1986}, - journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques}, - volume = {27}, - number = {2}, - pages = {133--146}, - url = {http://www.numdam.org/item/?id=CTGDC_1986__27_2_133_0}, - urldate = {2022-08-31}, - langid = {french}, - file = {/home/nerf/Zotero/storage/K5TFJMSJ/Borceux and Dejean - 1986 - Cauchy completion in category theory.pdf;/home/nerf/Zotero/storage/VQ499FFR/item.html} +@unpublished{riehlAlgebraicModelStructures2011, + title = {Algebraic Model Structures}, + author = {Riehl, Emily}, + date = {2011-03-11}, + eprint = {0910.2733}, + eprinttype = {arXiv}, + eprintclass = {math}, + url = {http://arxiv.org/abs/0910.2733}, + urldate = {2022-04-26}, + abstract = {We define a new notion of an algebraic model structure, in which the cofibrations and fibrations are retracts of coalgebras for comonads and algebras for monads, and prove "algebraic" analogs of classical results. Using a modified version of Quillen's small object argument, we show that every cofibrantly generated model structure in the usual sense underlies a cofibrantly generated algebraic model structure. We show how to pass a cofibrantly generated algebraic model structure across an adjunction, and we characterize the algebraic Quillen adjunction that results. We prove that pointwise natural weak factorization systems on diagram categories are cofibrantly generated if the original ones are, and we give an algebraic generalization of the projective model structure. Finally, we prove that certain fundamental comparison maps present in any cofibrantly generated model category are cofibrations when the cofibrations are monomorphisms, a conclusion that does not seem to be provable in the classical, non-algebraic, theory.}, + keywords = {55U35 18A32,Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/7748DLXS/Riehl - 2011 - Algebraic model structures.pdf;/home/nerf/Zotero/storage/5TLYJVHI/0910.html} } @article{bourkeAlgebraicWeakFactorisation2016, @@ -225,129 +122,47 @@ file = {/home/nerf/Zotero/storage/PY6J3T45/Bourke and Garner - 2016 - Algebraic weak factorisation systems II categorie.pdf;/home/nerf/Zotero/storage/5R23IT8L/1412.html} } -@online{castellanCategoriesFamiliesUnityped2020a, - title = {Categories with {{Families}}: {{Unityped}}, {{Simply Typed}}, and {{Dependently Typed}}}, - shorttitle = {Categories with {{Families}}}, - author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter}, - date = {2020-07-07}, - eprint = {1904.00827}, - eprinttype = {arXiv}, - eprintclass = {cs}, - doi = {10.48550/arXiv.1904.00827}, - url = {http://arxiv.org/abs/1904.00827}, - urldate = {2023-03-11}, - abstract = {We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.}, - pubstate = {prepublished}, - keywords = {Computer Science - Logic in Computer Science}, - file = {/home/nerf/Zotero/storage/D6MP7U8C/Castellan et al. - 2020 - Categories with Families Unityped, Simply Typed, .pdf;/home/nerf/Zotero/storage/9E9C3MVL/1904.html} -} - -@online{cavalloRelativeEleganceCartesian2022, - title = {Relative Elegance and Cartesian Cubes with One Connection}, - author = {Cavallo, Evan and Sattler, Christian}, - date = {2022-11-27}, - eprint = {2211.14801}, +@unpublished{isaacsonSymmetricCubicalSets2009, + title = {Symmetric {{Cubical Sets}}}, + author = {Isaacson, Samuel B.}, + date = {2009-10-26}, + eprint = {0910.4948}, eprinttype = {arXiv}, eprintclass = {math}, - doi = {10.48550/arXiv.2211.14801}, - url = {http://arxiv.org/abs/2211.14801}, - urldate = {2022-12-16}, - abstract = {We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a model of a cubical type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first known example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.}, - pubstate = {prepublished}, - keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/GH8VCM2Q/Cavallo and Sattler - 2022 - Relative elegance and cartesian cubes with one con.pdf;/home/nerf/Zotero/storage/75FUEPL2/2211.html} + url = {http://arxiv.org/abs/0910.4948}, + urldate = {2022-04-26}, + abstract = {We introduce a new cubical model for homotopy types. More precisely, we'll define a category Qs with the following features: Qs is a PROP containing the classical box category as a subcategory, the category Qs-Set of presheaves of sets on Qs models the homotopy category, and combinatorial symmetric monoidal model categories with cofibrant unit all have homotopically well behaved Qs-Set enrichments.}, + keywords = {55u35,Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/QGG5W5Q5/Isaacson - 2009 - Symmetric Cubical Sets.pdf;/home/nerf/Zotero/storage/ZN3NRQN4/0910.html} } -@article{cavalloUnifyingCubicalModels2016, - title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}}, - author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W}, - date = {2016}, - langid = {english}, - file = {/home/nerf/Zotero/storage/UDTLUHWA/Cavallo et al. - 2016 - Unifying Cubical Models of Univalent Type Theory.pdf} +@book{quillenHomotopicalAlgebra1967, + title = {Homotopical {{Algebra}}}, + author = {Quillen, Daniel G.}, + editor = {Dold, A. and Eckmann, B.}, + editortype = {redactor}, + date = {1967}, + series = {Lecture {{Notes}} in {{Mathematics}}}, + volume = {43}, + publisher = {Springer}, + location = {Berlin, Heidelberg}, + doi = {10.1007/BFb0097438}, + url = {http://link.springer.com/10.1007/BFb0097438}, + urldate = {2022-04-27}, + isbn = {978-3-540-03914-3 978-3-540-35523-6}, + keywords = {algebra,homotopical algebra,Homotopie,homotopy,homotopy theory,Quillen}, + file = {/home/nerf/Zotero/storage/JG33WVEZ/Quillen - 1967 - Homotopical Algebra.pdf} } -@inproceedings{cavalloUnifyingCubicalModels2020, - title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}}, - booktitle = {28th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2020)}, - author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W.}, - editor = {Fernández, Maribel and Muscholl, Anca}, - date = {2020}, - series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})}, - volume = {152}, - pages = {14:1--14:17}, - publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik}, - location = {Dagstuhl, Germany}, - issn = {1868-8969}, - doi = {10.4230/LIPIcs.CSL.2020.14}, - url = {https://drops.dagstuhl.de/opus/volltexte/2020/11657}, - urldate = {2023-08-23}, - isbn = {978-3-95977-132-0}, - keywords = {Cubical Set Models,Cubical Type Theory,examples composition structures,Homotopy Type Theory,Univalent Foundations}, - file = {/home/nerf/Zotero/storage/HMQ4GBI5/Cavallo et al. - 2020 - Unifying Cubical Models of Univalent Type Theory.pdf;/home/nerf/Zotero/storage/K2D9KNGG/11657.html} -} - -@online{CCHM, - title = {Cubical {{Type Theory}}: A Constructive Interpretation of the Univalence Axiom}, - shorttitle = {Cubical {{Type Theory}}}, - author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders}, - date = {2016-11-07}, - eprint = {1611.02108}, - eprinttype = {arXiv}, - eprintclass = {cs, math}, - doi = {10.48550/arXiv.1611.02108}, - url = {http://arxiv.org/abs/1611.02108}, - urldate = {2024-03-29}, - abstract = {This paper presents a type theory in which it is possible to directly manipulate \$n\$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, - pubstate = {prepublished}, - shorthand = {CCHM}, - keywords = {CCHM,Computer Science - Logic in Computer Science,de Morgan,F.3.2,F.4.1,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/IPGDN2AH/Cohen et al. - 2016 - Cubical Type Theory a constructive interpretation.pdf;/home/nerf/Zotero/storage/3Q8F527E/1611.html} -} - -@unpublished{coquandConstructiveSheafModels2020, - title = {Constructive Sheaf Models of Type Theory}, - author = {Coquand, Thierry and Ruch, Fabian and Sattler, Christian}, - date = {2020-07-08}, - eprint = {1912.10407}, - eprinttype = {arXiv}, - eprintclass = {math}, - url = {http://arxiv.org/abs/1912.10407}, - urldate = {2022-04-25}, - abstract = {We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.}, - keywords = {Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/BM86P38T/Coquand et al. - 2020 - Constructive sheaf models of type theory.pdf;/home/nerf/Zotero/storage/VIMEBY7W/1912.html} -} - -@online{coquandVariationCubicalSets2014, - title = {Variation on {{Cubical Sets}}}, - author = {Coquand, Thierry}, - date = {2014}, - url = {https://www.cse.chalmers.se/~coquand/diag.pdf}, - urldate = {2024-04-30}, - file = {/home/nerf/Zotero/storage/HQBY2TZY/diag.pdf} -} - -@online{dohertyCubicalModelsInfty2020, - title = {Cubical Models of \$(\textbackslash infty, 1)\$-Categories}, - author = {Doherty, Brandon and Kapulkin, Chris and Lindsey, Zachery and Sattler, Christian}, - date = {2020-05-11}, - url = {https://arxiv.org/abs/2005.04853v3}, - urldate = {2023-08-23}, - abstract = {We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK-equivalences.}, - langid = {english}, - organization = {arXiv.org}, - file = {/home/nerf/Zotero/storage/6F6WV5U3/Doherty et al. - 2020 - Cubical models of $(infty, 1)$-categories.pdf} -} - -@inproceedings{dybjerInternalTypeTheory2003, - title = {Internal {{Type Theory}}}, - author = {Dybjer, Peter}, - date = {2003-06-23}, - doi = {10.1007/3-540-61780-9_66}, - abstract = {We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also present categories with families as a generalized algebraic theory. Then we define categories with families formally in Martin-Lof's intensional intuitionistic type theory. Finally, we discuss the coherence problem for these internal categories with families.}, - isbn = {978-3-540-61780-8}, - keywords = {CwF,Families}, - file = {/home/nerf/Zotero/storage/MKQRDD7X/Dybjer - 2003 - Internal Type Theory.pdf} +@article{grandisNaturalWeakFactorization2006, + title = {Natural Weak Factorization Systems}, + author = {Grandis, Marco and Tholen, Walter}, + date = {2006-01-01}, + journaltitle = {Archivum Mathematicum}, + shortjournal = {Archivum Mathematicum}, + volume = {42}, + abstract = {In order to facilitate a natural choice for morphisms created by the (left or right) lifting property as used in the definition of weak factorization systems, the notion of natural weak factorization system in the category K is introduced, as a pair (comonad, monad) over K 2 . The link with existing notions in terms of morphism classes is given via the respective Eilenberg–Moore categories.}, + file = {/home/nerf/Zotero/storage/PKDDLPTE/Grandis and Tholen - 2006 - Natural weak factorization systems.pdf} } @unpublished{gambinoConstructiveKanQuillenModel2021, @@ -365,20 +180,6 @@ file = {/home/nerf/Zotero/storage/G66J48KN/Gambino et al. - 2021 - The constructive Kan-Quillen model structure two .pdf;/home/nerf/Zotero/storage/IQ2BSHPM/1907.html} } -@unpublished{gambinoEffectiveModelStructure2021, - title = {The Effective Model Structure and \$\textbackslash infty\$-Groupoid Objects}, - author = {Gambino, Nicola and Henry, Simon and Sattler, Christian and Szumiło, Karol}, - date = {2021-03-10}, - eprint = {2102.06146}, - eprinttype = {arXiv}, - eprintclass = {math}, - url = {http://arxiv.org/abs/2102.06146}, - urldate = {2022-04-25}, - abstract = {For a category \$\textbackslash mathcal E\$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in \$\textbackslash mathcal E\$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated \$\textbackslash infty\$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when \$\textbackslash mathcal E\$ is, but is not a higher topos in general. We also characterise the \$\textbackslash infty\$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on \$\textbackslash mathcal E\$ spanned by Kan complexes in \$\textbackslash mathcal E\$, a result that suggests a close analogy with the theory of exact completions.}, - keywords = {18N40 (primary) 18N60 55U10,Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/QVGLME2U/Gambino et al. - 2021 - The effective model structure and $infty$-groupoi.pdf;/home/nerf/Zotero/storage/2YSZT8KA/2102.html} -} - @article{gambinoFrobeniusConditionRight2017, title = {The {{Frobenius Condition}}, {{Right Properness}}, and {{Uniform Fibrations}}}, author = {Gambino, Nicola and Sattler, Christian}, @@ -399,56 +200,80 @@ file = {/home/nerf/Zotero/storage/SVIAPJW5/Gambino and Sattler - 2017 - The Frobenius Condition, Right Properness, and Uni.pdf;/home/nerf/Zotero/storage/DTMPA7ZW/1510.html;/home/nerf/Zotero/storage/NLPL6A6T/1510.html} } -@article{gambinoPolynomialFunctorsPolynomial2013, - title = {Polynomial Functors and Polynomial Monads}, - author = {Gambino, Nicola and Kock, Joachim}, - date = {2013-01}, - journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society}, - shortjournal = {Math. Proc. Camb. Phil. Soc.}, - volume = {154}, - number = {1}, - eprint = {0906.4931}, +@unpublished{LOPS, + title = {Internal {{Universes}} in {{Models}} of {{Homotopy Type Theory}}}, + author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas}, + date = {2018}, + eprint = {1801.07664}, eprinttype = {arXiv}, - eprintclass = {math}, - pages = {153--192}, - issn = {0305-0041, 1469-8064}, - doi = {10.1017/S0305004112000394}, - url = {http://arxiv.org/abs/0906.4931}, - urldate = {2024-08-04}, - abstract = {We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.}, - keywords = {18C15 18D05 18D50 03G30,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/JMIDZIWR/Gambino and Kock - 2013 - Polynomial functors and polynomial monads.pdf;/home/nerf/Zotero/storage/CADCALSE/0906.html} + eprintclass = {cs}, + pages = {17 pages}, + doi = {10.4230/LIPIcs.FSCD.2018.22}, + url = {http://arxiv.org/abs/1801.07664}, + urldate = {2022-05-11}, + abstract = {We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-M\textbackslash "ortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.}, + shorthand = {LOPS}, + version = {2}, + keywords = {Computer Science - Logic in Computer Science,F.3.2,F.4.1,LOPS,Tiny}, + file = {/home/nerf/Zotero/storage/58IRMAVX/Licata et al. - 2018 - Internal Universes in Models of Homotopy Type Theo.pdf;/home/nerf/Zotero/storage/9H5DEUV7/1801.html} } -@article{garnerUnderstandingSmallObject2009, - title = {Understanding the Small Object Argument}, - author = {Garner, Richard}, - date = {2009-06}, - journaltitle = {Applied Categorical Structures}, - shortjournal = {Appl Categor Struct}, - volume = {17}, - number = {3}, - eprint = {0712.0724}, +@unpublished{ortonAxiomsModellingCubical2018, + title = {Axioms for {{Modelling Cubical Type Theory}} in a {{Topos}}}, + author = {Orton, Ian and Pitts, Andrew M.}, + date = {2018-12-08}, + eprint = {1712.04864}, eprinttype = {arXiv}, - pages = {247--285}, - issn = {0927-2852, 1572-9095}, - doi = {10.1007/s10485-008-9137-4}, - url = {http://arxiv.org/abs/0712.0724}, - urldate = {2022-04-26}, - abstract = {The small object argument is a transfinite construction which, starting from a set of maps in a category, generates a weak factorisation system on that category. As useful as it is, the small object argument has some problematic aspects: it possesses no universal property; it does not converge; and it does not seem to be related to other transfinite constructions occurring in categorical algebra. In this paper, we give an "algebraic" refinement of the small object argument, cast in terms of Grandis and Tholen's natural weak factorisation systems, which rectifies each of these three deficiencies.}, - keywords = {18A32 55U35,18C10,55U35,Algebraic model structures,Mathematics - Algebraic Topology,Mathematics - Category Theory,Small object argument,Weak factorisation system}, - file = {/home/nerf/Zotero/storage/7UVP29D5/Garner - 2009 - Understanding the Small Object Argument.pdf;/home/nerf/Zotero/storage/9V4MZU3G/Garner - 2009 - Understanding the small object argument.pdf;/home/nerf/Zotero/storage/8TPNVUAK/0712.html} + eprintclass = {cs}, + doi = {10.23638/LMCS-14(4:23)2018}, + url = {http://arxiv.org/abs/1712.04864}, + urldate = {2022-05-11}, + abstract = {The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object \$I\$ in a topos to give such a path-based model of type theory in which paths are just functions with domain \$I\$. Cohen, Coquand, Huber and M\textbackslash "ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)}, + keywords = {Computer Science - Logic in Computer Science,F.4.1}, + file = {/home/nerf/Zotero/storage/IPQSVWQ9/Orton and Pitts - 2018 - Axioms for Modelling Cubical Type Theory in a Topo.pdf;/home/nerf/Zotero/storage/KRK2SGUB/1712.html} } -@article{grandisNaturalWeakFactorization2006, - title = {Natural Weak Factorization Systems}, - author = {Grandis, Marco and Tholen, Walter}, - date = {2006-01-01}, - journaltitle = {Archivum Mathematicum}, - shortjournal = {Archivum Mathematicum}, - volume = {42}, - abstract = {In order to facilitate a natural choice for morphisms created by the (left or right) lifting property as used in the definition of weak factorization systems, the notion of natural weak factorization system in the category K is introduced, as a pair (comonad, monad) over K 2 . The link with existing notions in terms of morphism classes is given via the respective Eilenberg–Moore categories.}, - file = {/home/nerf/Zotero/storage/PKDDLPTE/Grandis and Tholen - 2006 - Natural weak factorization systems.pdf} +@article{awodeyQuillenModelStructures, + title = {Quillen Model Structures on Cubical Sets}, + author = {Awodey, Steve}, + pages = {31}, + langid = {english}, + file = {/home/nerf/Zotero/storage/79HSXCBI/Awodey - Quillen model structures on cubical sets.pdf} +} + +@video{riehlVid, + entrysubtype = {video}, + title = {The {{Equivariant Uniform Kan Fibration Model}} of {{Cubical Homotopy Type Theory}} - {{YouTube}}}, + editor = {Riehl, Emily}, + editortype = {director}, + date = {2020-05-26}, + url = {https://www.youtube.com/watch?v=A8tEwxM7uxE}, + urldate = {2022-06-19}, + abstract = {Dr Emily Riehl Johns Hopkins University}, + file = {/home/nerf/Zotero/storage/SYCCCLDV/watch.html} +} + +@article{borceuxCauchyCompletionCategory1986, + title = {Cauchy completion in category theory}, + author = {Borceux, Francis and Dejean, Dominique}, + date = {1986}, + journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques}, + volume = {27}, + number = {2}, + pages = {133--146}, + url = {http://www.numdam.org/item/?id=CTGDC_1986__27_2_133_0}, + urldate = {2022-08-31}, + langid = {french}, + file = {/home/nerf/Zotero/storage/K5TFJMSJ/Borceux and Dejean - 1986 - Cauchy completion in category theory.pdf;/home/nerf/Zotero/storage/VQ499FFR/item.html} +} + +@article{riehlTOPOSSEMANTICSHOMOTOPY, + title = {{{ON THE}} ∞-{{TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY}}}, + author = {Riehl, Emily}, + pages = {37}, + abstract = {Many introductions to homotopy type theory and the univalence axiom neglect to explain what any of it means, glossing over the semantics of this new formal system in traditional set-based foundations. This series of talks will attempt to survey the state of the art, first presenting Voevodsky’s simplicial model of univalent foundations and then touring Shulman’s vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ∞-topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.}, + langid = {english}, + file = {/home/nerf/Zotero/storage/UA9ZRJ5Y/Riehl - ON THE ∞-TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY.pdf} } @online{gratzerStrictUniversesGrothendieck2022, @@ -467,20 +292,56 @@ file = {/home/nerf/Zotero/storage/IREIT5EI/Gratzer et al. - 2022 - Strict universes for Grothendieck topoi.pdf;/home/nerf/Zotero/storage/QZ4LQ95R/2202.html} } -@book{hirschhornModelCategoriesTheir2009, - title = {Model {{Categories}} and {{Their Localizations}}}, - author = {Hirschhorn, Philip}, - date = {2009-08-24}, - series = {Mathematical {{Surveys}} and {{Monographs}}}, - volume = {99}, - publisher = {American Mathematical Society}, - issn = {0076-5376, 2331-7159}, - doi = {10.1090/surv/099}, - url = {https://www.ams.org/surv/099}, - urldate = {2023-09-12}, - abstract = {Advancing research. Creating connections.}, - isbn = {978-0-8218-4917-0 978-1-4704-1326-2}, - langid = {english} +@online{cavalloRelativeEleganceCartesian2022, + title = {Relative Elegance and Cartesian Cubes with One Connection}, + author = {Cavallo, Evan and Sattler, Christian}, + date = {2022-11-27}, + eprint = {2211.14801}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.2211.14801}, + url = {http://arxiv.org/abs/2211.14801}, + urldate = {2022-12-16}, + abstract = {We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a model of a cubical type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first known example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.}, + pubstate = {prepublished}, + keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/GH8VCM2Q/Cavallo and Sattler - 2022 - Relative elegance and cartesian cubes with one con.pdf;/home/nerf/Zotero/storage/75FUEPL2/2211.html} +} + +@online{castellanCategoriesFamiliesUnityped2020a, + title = {Categories with {{Families}}: {{Unityped}}, {{Simply Typed}}, and {{Dependently Typed}}}, + shorttitle = {Categories with {{Families}}}, + author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter}, + date = {2020-07-07}, + eprint = {1904.00827}, + eprinttype = {arXiv}, + eprintclass = {cs}, + doi = {10.48550/arXiv.1904.00827}, + url = {http://arxiv.org/abs/1904.00827}, + urldate = {2023-03-11}, + abstract = {We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.}, + pubstate = {prepublished}, + keywords = {Computer Science - Logic in Computer Science}, + file = {/home/nerf/Zotero/storage/D6MP7U8C/Castellan et al. - 2020 - Categories with Families Unityped, Simply Typed, .pdf;/home/nerf/Zotero/storage/9E9C3MVL/1904.html} +} + +@article{ABCHFL, + title = {Syntax and Models of {{Cartesian}} Cubical Type Theory}, + author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Harper, Robert and Hou (Favonia), Kuen-Bang and Licata, Daniel R.}, + date = {2021-04}, + journaltitle = {Mathematical Structures in Computer Science}, + volume = {31}, + number = {4}, + pages = {424--468}, + publisher = {Cambridge University Press}, + issn = {0960-1295, 1469-8072}, + doi = {10.1017/S0960129521000347}, + url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/syntax-and-models-of-cartesian-cubical-type-theory/01B9E98DF997F0861E4BA13A34B72A7D}, + urldate = {2023-04-21}, + abstract = {We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.}, + langid = {english}, + keywords = {ABCHFL,cubical type theory,homotopy type theory,Type theory}, + file = {/home/nerf/Zotero/storage/2MPEKIEC/Angiuli et al. - 2021 - Syntax and models of Cartesian cubical type theory.pdf} } @article{hofmannDoctorPhilosophyUniversity, @@ -490,78 +351,6 @@ file = {/home/nerf/Zotero/storage/VKM9TK2D/Hofmann - Doctor of Philosophy University of Edinburgh 1995.pdf} } -@article{hofmannLiftingGrothendieckUniverses1997, - title = {Lifting {{Grothendieck Universes}}}, - author = {Hofmann, Martin and Streicher, Thomas}, - date = {1997-21}, - url = {https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf}, - langid = {english}, - file = {/home/nerf/Zotero/storage/LE9B8IMD/Hofmann et al. - Lifting Grothendieck Universes.pdf} -} - -@article{hofmannSyntaxSemanticsDependent, - title = {Syntax and {{Semantics}} of {{Dependent Types}}}, - author = {Hofmann, Martin}, - langid = {english}, - keywords = {CwF,Families,Presheaf model}, - file = {/home/nerf/Zotero/storage/NY2W23FP/Hofmann - Syntax and Semantics of Dependent Types.pdf} -} - -@online{hoveyModelCategories2007, - title = {Model {{Categories}}}, - author = {Hovey, Mark}, - date = {2007-10-17}, - series = {Mathematical {{Surveys}} and {{Monographs}}}, - volume = {63}, - publisher = {American Mathematical Society}, - issn = {0076-5376, 2331-7159}, - doi = {10.1090/surv/063}, - url = {https://www.ams.org/surv/063}, - urldate = {2024-04-28}, - abstract = {Advancing research. Creating connections.}, - isbn = {9780821843611 9781470412906}, - langid = {english}, - organization = {American Mathematical Society} -} - -@online{hoveyModelCategories2007a, - title = {Model {{Categories}}}, - author = {Hovey, Mark}, - date = {2007-10-17}, - series = {Mathematical {{Surveys}} and {{Monographs}}}, - volume = {63}, - publisher = {American Mathematical Society}, - issn = {0076-5376, 2331-7159}, - doi = {10.1090/surv/063}, - url = {https://www.ams.org/surv/063}, - urldate = {2024-08-02}, - abstract = {Advancing research. Creating connections.}, - isbn = {9780821843611 9781470412906}, - langid = {english}, - organization = {American Mathematical Society} -} - -@online{IntroductionHomotopyTheory, - title = {Introduction to {{Homotopy Theory}} in {{nLab}}}, - url = {https://ncatlab.org/nlab/show/Introduction+to+Homotopy+Theory}, - urldate = {2023-09-12}, - file = {/home/nerf/Zotero/storage/77QL5DY8/Introduction+to+Homotopy+Theory.html} -} - -@unpublished{isaacsonSymmetricCubicalSets2009, - title = {Symmetric {{Cubical Sets}}}, - author = {Isaacson, Samuel B.}, - date = {2009-10-26}, - eprint = {0910.4948}, - eprinttype = {arXiv}, - eprintclass = {math}, - url = {http://arxiv.org/abs/0910.4948}, - urldate = {2022-04-26}, - abstract = {We introduce a new cubical model for homotopy types. More precisely, we'll define a category Qs with the following features: Qs is a PROP containing the classical box category as a subcategory, the category Qs-Set of presheaves of sets on Qs models the homotopy category, and combinatorial symmetric monoidal model categories with cofibrant unit all have homotopically well behaved Qs-Set enrichments.}, - keywords = {55u35,Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/QGG5W5Q5/Isaacson - 2009 - Symmetric Cubical Sets.pdf;/home/nerf/Zotero/storage/ZN3NRQN4/0910.html} -} - @book{jacobsCategoricalLogicType1999, title = {Categorical Logic and Type Theory}, author = {Jacobs, Bart}, @@ -578,6 +367,208 @@ file = {/home/nerf/Zotero/storage/BKE5ASHQ/Jacobs - 1999 - Categorical logic and type theory.pdf} } +@book{riehlCategoricalHomotopyTheory2014, + title = {Categorical {{Homotopy Theory}}}, + author = {Riehl, Emily}, + date = {2014}, + series = {New {{Mathematical Monographs}}}, + publisher = {Cambridge University Press}, + location = {Cambridge}, + doi = {10.1017/CBO9781107261457}, + url = {https://www.cambridge.org/core/books/categorical-homotopy-theory/556C7A200B521E61466BB7763C49DDA4}, + urldate = {2023-07-07}, + abstract = {This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: either as derived functors definable when the appropriate diagram categories admit a compatible model structure, or through particular formulae that give the right notion in certain examples. Emily Riehl unifies these seemingly rival perspectives and demonstrates that model structures on diagram categories are irrelevant. Homotopy (co)limits are explained to be a special case of weighted (co)limits, a foundational topic in enriched category theory. In Part II, Riehl further examines this topic, separating categorical arguments from homotopical ones. Part III treats the most ubiquitous axiomatic framework for homotopy theory - Quillen's model categories. Here, Riehl simplifies familiar model categorical lemmas and definitions by focusing on weak factorization systems. Part IV introduces quasi-categories and homotopy coherence.}, + isbn = {978-1-107-04845-4}, + file = {/home/nerf/Zotero/storage/NEXTFSKD/Riehl - Categorical homotopy theory.pdf;/home/nerf/Zotero/storage/IJYSYMC6/556C7A200B521E61466BB7763C49DDA4.html} +} + +@online{sattlerIdempotentCompletionCubes2019, + title = {Idempotent Completion of Cubes in Posets}, + author = {Sattler, Christian}, + date = {2019-03-08}, + eprint = {1805.04126}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.1805.04126}, + url = {http://arxiv.org/abs/1805.04126}, + urldate = {2023-08-23}, + abstract = {This note concerns the category \$\textbackslash Box\$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects \$[1]\textasciicircum n\$ with \$n \textbackslash geq 0\$. We show that the idempotent completion of \$\textbackslash Box\$ consists of finite complete posets. It follows that cubical sets, ie presheaves over \$\textbackslash Box\$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.}, + pubstate = {prepublished}, + keywords = {Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/SYH7C9JV/Sattler - 2019 - Idempotent completion of cubes in posets.pdf;/home/nerf/Zotero/storage/9ZN8RBCZ/1805.html} +} + +@online{sattlerEquivalenceExtensionProperty2017, + title = {The {{Equivalence Extension Property}} and {{Model Structures}}}, + author = {Sattler, Christian}, + date = {2017-04-23}, + url = {https://arxiv.org/abs/1704.06911v4}, + urldate = {2023-08-23}, + abstract = {We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex\textasciicircum infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.}, + langid = {english}, + pubstate = {prepublished}, + keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,The unknown Paper?}, + file = {/home/nerf/Zotero/storage/GFLT3HLU/Sattler - 2017 - The Equivalence Extension Property and Model Struc.pdf;/home/nerf/Zotero/storage/FDPHZXNP/1704.html;/home/nerf/Zotero/storage/SEADD4R7/1704.html} +} + +@online{dohertyCubicalModelsInfty2020, + title = {Cubical Models of \$(\textbackslash infty, 1)\$-Categories}, + author = {Doherty, Brandon and Kapulkin, Chris and Lindsey, Zachery and Sattler, Christian}, + date = {2020-05-11}, + url = {https://arxiv.org/abs/2005.04853v3}, + urldate = {2023-08-23}, + abstract = {We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK-equivalences.}, + langid = {english}, + organization = {arXiv.org}, + file = {/home/nerf/Zotero/storage/6F6WV5U3/Doherty et al. - 2020 - Cubical models of $(infty, 1)$-categories.pdf} +} + +@inproceedings{cavalloUnifyingCubicalModels2020, + title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}}, + booktitle = {28th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2020)}, + author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W.}, + editor = {Fernández, Maribel and Muscholl, Anca}, + date = {2020}, + series = {Leibniz {{International Proceedings}} in {{Informatics}} ({{LIPIcs}})}, + volume = {152}, + pages = {14:1--14:17}, + publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik}, + location = {Dagstuhl, Germany}, + issn = {1868-8969}, + doi = {10.4230/LIPIcs.CSL.2020.14}, + url = {https://drops.dagstuhl.de/opus/volltexte/2020/11657}, + urldate = {2023-08-23}, + isbn = {978-3-95977-132-0}, + keywords = {Cubical Set Models,Cubical Type Theory,examples composition structures,Homotopy Type Theory,Univalent Foundations}, + file = {/home/nerf/Zotero/storage/HMQ4GBI5/Cavallo et al. - 2020 - Unifying Cubical Models of Univalent Type Theory.pdf;/home/nerf/Zotero/storage/K2D9KNGG/11657.html} +} + +@inproceedings{bezemModelTypeTheory2014, + title = {A {{Model}} of {{Type Theory}} in {{Cubical Sets}}}, + author = {Bezem, Marc and Coquand, Thierry and Huber, Simon}, + namea = {Herbstritt, Marc}, + nameatype = {collaborator}, + date = {2014}, + pages = {22 pages}, + publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany}, + doi = {10.4230/LIPICS.TYPES.2013.107}, + url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628/}, + urldate = {2023-08-28}, + abstract = {We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.}, + langid = {english}, + keywords = {000 Computer science knowledge general works,Computer Science}, + file = {/home/nerf/Zotero/storage/4KKXST7S/Bezem et al. - A model of type theory in cubical sets.pdf} +} + +@inproceedings{dybjerInternalTypeTheory2003, + title = {Internal {{Type Theory}}}, + author = {Dybjer, Peter}, + date = {2003-06-23}, + doi = {10.1007/3-540-61780-9_66}, + abstract = {We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also present categories with families as a generalized algebraic theory. Then we define categories with families formally in Martin-Lof's intensional intuitionistic type theory. Finally, we discuss the coherence problem for these internal categories with families.}, + isbn = {978-3-540-61780-8}, + keywords = {CwF,Families}, + file = {/home/nerf/Zotero/storage/MKQRDD7X/Dybjer - 2003 - Internal Type Theory.pdf} +} + +@book{streicherSemanticsTypeTheory1991, + title = {Semantics of {{Type Theory}}}, + author = {Streicher, Thomas}, + date = {1991}, + publisher = {Birkhäuser Boston}, + location = {Boston, MA}, + doi = {10.1007/978-1-4612-0433-6}, + url = {http://link.springer.com/10.1007/978-1-4612-0433-6}, + urldate = {2023-09-02}, + isbn = {978-1-4612-6757-7 978-1-4612-0433-6}, + langid = {english}, + file = {/home/nerf/Zotero/storage/ALA3AMGY/Streicher - 1991 - Semantics of Type Theory.pdf} +} + +@article{hofmannSyntaxSemanticsDependent, + title = {Syntax and {{Semantics}} of {{Dependent Types}}}, + author = {Hofmann, Martin}, + langid = {english}, + keywords = {CwF,Families,Presheaf model}, + file = {/home/nerf/Zotero/storage/NY2W23FP/Hofmann - Syntax and Semantics of Dependent Types.pdf} +} + +@book{maclaneCategoriesWorkingMathematician1978, + title = {Categories for the {{Working Mathematician}}}, + author = {Mac Lane, Saunders}, + date = {1978}, + series = {Graduate {{Texts}} in {{Mathematics}}}, + volume = {5}, + publisher = {Springer}, + location = {New York, NY}, + doi = {10.1007/978-1-4757-4721-8}, + url = {http://link.springer.com/10.1007/978-1-4757-4721-8}, + urldate = {2023-09-12}, + isbn = {978-1-4419-3123-8 978-1-4757-4721-8}, + keywords = {addition,Adjoint functor,algebra,Morphism,theorem}, + file = {/home/nerf/Zotero/storage/LCQ4M4Q8/Mac Lane - 1978 - Categories for the Working Mathematician.pdf} +} + +@book{awodeyCategoryTheory2006, + title = {Category {{Theory}}}, + author = {Awodey, Steve}, + date = {2006-05-25}, + publisher = {Oxford University Press}, + doi = {10.1093/acprof:oso/9780198568612.001.0001}, + url = {https://doi.org/10.1093/acprof:oso/9780198568612.001.0001}, + urldate = {2023-09-12}, + abstract = {This book is a text and reference book on Category Theory, a branch of abstract algebra. The book contains clear definitions of the essential concepts, which are illuminated with numerous accessible examples. It provides full proofs of all the important propositions and theorems, and aims to make the basic ideas, theorems, and methods of Category Theory understandable. Although it assumes few mathematical pre-requisites, the standard of mathematical rigour is not compromised. The material covered includes the standard core of categories; functors; natural transformations; equivalence; limits and colimits; functor categories; representables; Yoneda's lemma; adjoints; and monads. An extra topic of cartesian closed categories and the lambda-calculus is also provided.}, + isbn = {978-0-19-856861-2} +} + +@book{maclaneSheavesGeometryLogic1994, + title = {Sheaves in {{Geometry}} and {{Logic}}: {{A First Introduction}} to {{Topos Theory}}}, + shorttitle = {Sheaves in {{Geometry}} and {{Logic}}}, + author = {Mac Lane, Saunders and Moerdijk, Ieke}, + date = {1994}, + series = {Universitext}, + publisher = {Springer}, + location = {New York, NY}, + doi = {10.1007/978-1-4612-0927-0}, + url = {https://link.springer.com/10.1007/978-1-4612-0927-0}, + urldate = {2023-09-12}, + isbn = {978-0-387-97710-2 978-1-4612-0927-0}, + langid = {english}, + keywords = {Algebraic structure,Boolean algebra,Division,forcing,Heyting algebra,set,set theory}, + file = {/home/nerf/Zotero/storage/W58HYMXM/Mac Lane and Moerdijk - 1994 - Sheaves in Geometry and Logic A First Introductio.pdf} +} + +@online{IntroductionHomotopyTheory, + title = {Introduction to {{Homotopy Theory}} in {{nLab}}}, + url = {https://ncatlab.org/nlab/show/Introduction+to+Homotopy+Theory}, + urldate = {2023-09-12}, + file = {/home/nerf/Zotero/storage/77QL5DY8/Introduction+to+Homotopy+Theory.html} +} + +@book{hirschhornModelCategoriesTheir2009, + title = {Model {{Categories}} and {{Their Localizations}}}, + author = {Hirschhorn, Philip}, + date = {2009-08-24}, + series = {Mathematical {{Surveys}} and {{Monographs}}}, + volume = {99}, + publisher = {American Mathematical Society}, + issn = {0076-5376, 2331-7159}, + doi = {10.1090/surv/099}, + url = {https://www.ams.org/surv/099}, + urldate = {2023-09-12}, + abstract = {Advancing research. Creating connections.}, + isbn = {978-0-8218-4917-0 978-1-4704-1326-2}, + langid = {english} +} + +@article{cavalloUnifyingCubicalModels2016, + title = {Unifying {{Cubical Models}} of {{Univalent Type Theory}}}, + author = {Cavallo, Evan and Mörtberg, Anders and Swan, Andrew W}, + date = {2016}, + langid = {english}, + file = {/home/nerf/Zotero/storage/UDTLUHWA/Cavallo et al. - 2016 - Unifying Cubical Models of Univalent Type Theory.pdf} +} + @inbook{lawvereAlgebraicProblemsContext1968, title = {Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories}, booktitle = {Reports of the {{Midwest Category Seminar II}}}, @@ -614,55 +605,137 @@ file = {/home/nerf/Zotero/storage/ECTRWE4B/Lawvere - 1963 - FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES.pdf} } -@unpublished{LOPS, - title = {Internal {{Universes}} in {{Models}} of {{Homotopy Type Theory}}}, - author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas}, - date = {2018}, - eprint = {1801.07664}, - eprinttype = {arXiv}, - eprintclass = {cs}, - pages = {17 pages}, - doi = {10.4230/LIPIcs.FSCD.2018.22}, - url = {http://arxiv.org/abs/1801.07664}, - urldate = {2022-05-11}, - abstract = {We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-M\textbackslash "ortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.}, - shorthand = {LOPS}, - version = {2}, - keywords = {Computer Science - Logic in Computer Science,F.3.2,F.4.1,LOPS,Tiny}, - file = {/home/nerf/Zotero/storage/58IRMAVX/Licata et al. - 2018 - Internal Universes in Models of Homotopy Type Theo.pdf;/home/nerf/Zotero/storage/9H5DEUV7/1801.html} -} - -@book{maclaneCategoriesWorkingMathematician1978, - title = {Categories for the {{Working Mathematician}}}, - author = {Mac Lane, Saunders}, - date = {1978}, - series = {Graduate {{Texts}} in {{Mathematics}}}, - volume = {5}, - publisher = {Springer}, - location = {New York, NY}, - doi = {10.1007/978-1-4757-4721-8}, - url = {http://link.springer.com/10.1007/978-1-4757-4721-8}, - urldate = {2023-09-12}, - isbn = {978-1-4419-3123-8 978-1-4757-4721-8}, - keywords = {addition,Adjoint functor,algebra,Morphism,theorem}, - file = {/home/nerf/Zotero/storage/LCQ4M4Q8/Mac Lane - 1978 - Categories for the Working Mathematician.pdf} -} - -@book{maclaneSheavesGeometryLogic1994, - title = {Sheaves in {{Geometry}} and {{Logic}}: {{A First Introduction}} to {{Topos Theory}}}, - shorttitle = {Sheaves in {{Geometry}} and {{Logic}}}, - author = {Mac Lane, Saunders and Moerdijk, Ieke}, - date = {1994}, - series = {Universitext}, - publisher = {Springer}, - location = {New York, NY}, - doi = {10.1007/978-1-4612-0927-0}, - url = {https://link.springer.com/10.1007/978-1-4612-0927-0}, - urldate = {2023-09-12}, - isbn = {978-0-387-97710-2 978-1-4612-0927-0}, +@incollection{streicherUNIVERSESTOPOSES2005, + title = {{{UNIVERSES IN TOPOSES}}}, + booktitle = {From {{Sets}} and {{Types}} to {{Topology}} and {{Analysis}}}, + author = {Streicher, Thomas}, + editor = {Crosilla, Laura and Schuster, Peter}, + date = {2005-10-06}, + edition = {1}, + pages = {78--90}, + publisher = {Oxford University PressOxford}, + doi = {10.1093/acprof:oso/9780198566519.003.0005}, + url = {https://academic.oup.com/book/5354/chapter/148144921}, + urldate = {2023-11-14}, + abstract = {We discuss a notion of universe in toposes which from a logical point of view gives rise to an extension of Higher Order Intuitionistic Arithmetic (HAH) that allows one to construct families of types in such a universe by structural recursion and to quantify over such families. Further, we show that (hierarchies of) such universes do exist in all sheaf and realizability toposes but neither in the free topos nor in the Vω+ω model of Zermelo set theory.}, + isbn = {978-0-19-856651-9 978-0-19-171392-7}, langid = {english}, - keywords = {Algebraic structure,Boolean algebra,Division,forcing,Heyting algebra,set,set theory}, - file = {/home/nerf/Zotero/storage/W58HYMXM/Mac Lane and Moerdijk - 1994 - Sheaves in Geometry and Logic A First Introductio.pdf} + file = {/home/nerf/Zotero/storage/CB5TH6EV/Streicher - 2005 - UNIVERSES IN TOPOSES.pdf} +} + +@online{awodeyKripkeJoyalForcingType2021, + title = {Kripke-{{Joyal}} Forcing for Type Theory and Uniform Fibrations}, + author = {Awodey, S. and Gambino, N. and Hazratpour, S.}, + date = {2021-10-27}, + eprint = {2110.14576}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.2110.14576}, + url = {http://arxiv.org/abs/2110.14576}, + urldate = {2024-02-21}, + abstract = {We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.}, + pubstate = {prepublished}, + keywords = {03G30 03B38 18F20 18N45,Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/NNQITW4X/Awodey et al. - 2021 - Kripke-Joyal forcing for type theory and uniform f.pdf;/home/nerf/Zotero/storage/M3MTFM97/2110.html} +} + +@online{swanDefinableNondefinableNotions2022, + title = {Definable and {{Non-definable Notions}} of {{Structure}}}, + author = {Swan, Andrew W.}, + date = {2022-06-27}, + eprint = {2206.13643}, + eprinttype = {arXiv}, + eprintclass = {cs, math}, + doi = {10.48550/arXiv.2206.13643}, + url = {http://arxiv.org/abs/2206.13643}, + urldate = {2024-03-11}, + abstract = {Definability is a key notion in the theory of Grothendieck fibrations that characterises when an external property of objects can be accessed from within the internal logic of the base of a fibration. In this paper we consider a generalisation of definability from properties of objects to structures on objects, introduced by Shulman under the name local representability. We first develop some general theory and show how to recover existing notions due to B\textbackslash '\{e\}nabou and Johnstone as special cases. We give several examples of definable and non definable notions o structure, focusing on algebraic weak factorisation systems, which can be naturally viewed as notions of structure on codomain fibrations. Regarding definability, we give a sufficient criterion for cofibrantly generated awfs's to be definable, generalising a construction of the universe for cubical sets, but also including some very different looking examples that do not satisfy tininess in the internal sense, that exponential functors have a right adjoint. Our examples of non definability include the identification of logical principles holding for the interval objects in simplicial sets and Bezem-Coquand-Huber cubical sets that suffice to show a certain definition of Kan fibration is not definable.}, + pubstate = {prepublished}, + keywords = {03G30 18N40,Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/CJRDB5DU/Swan - 2022 - Definable and Non-definable Notions of Structure.pdf;/home/nerf/Zotero/storage/DS7C3TKZ/2206.html} +} + +@online{rileyTypeTheoryTiny2024, + title = {A {{Type Theory}} with a {{Tiny Object}}}, + author = {Riley, Mitchell}, + date = {2024-03-04}, + eprint = {2403.01939}, + eprinttype = {arXiv}, + eprintclass = {cs, math}, + doi = {10.48550/arXiv.2403.01939}, + url = {http://arxiv.org/abs/2403.01939}, + urldate = {2024-03-12}, + abstract = {We present an extension of Martin-L\textbackslash "of Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected left adjoint. We demonstrate the practicality of this type theory by proving various properties related to tininess internally and suggest a few potential applications.}, + pubstate = {prepublished}, + keywords = {Computer Science - Programming Languages,Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/DM45P9J4/Riley - 2024 - A Type Theory with a Tiny Object.pdf;/home/nerf/Zotero/storage/8KAP7SMU/2403.html} +} + +@article{riehlCategoryTheoryContext, + title = {Category Theory in Context}, + author = {Riehl, Emily}, + langid = {english}, + file = {/home/nerf/Zotero/storage/4WNNYCP7/Riehl - Category theory in context.pdf} +} + +@online{CCHM, + title = {Cubical {{Type Theory}}: A Constructive Interpretation of the Univalence Axiom}, + shorttitle = {Cubical {{Type Theory}}}, + author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders}, + date = {2016-11-07}, + eprint = {1611.02108}, + eprinttype = {arXiv}, + eprintclass = {cs, math}, + doi = {10.48550/arXiv.1611.02108}, + url = {http://arxiv.org/abs/1611.02108}, + urldate = {2024-03-29}, + abstract = {This paper presents a type theory in which it is possible to directly manipulate \$n\$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, + pubstate = {prepublished}, + shorthand = {CCHM}, + keywords = {CCHM,Computer Science - Logic in Computer Science,de Morgan,F.3.2,F.4.1,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/IPGDN2AH/Cohen et al. - 2016 - Cubical Type Theory a constructive interpretation.pdf;/home/nerf/Zotero/storage/3Q8F527E/1611.html} +} + +@online{riehlTheoryPracticeReedy2014, + title = {The Theory and Practice of {{Reedy}} Categories}, + author = {Riehl, Emily and Verity, Dominic}, + date = {2014-06-03}, + eprint = {1304.6871}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.1304.6871}, + url = {http://arxiv.org/abs/1304.6871}, + urldate = {2024-04-07}, + abstract = {The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but difficult to find in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Specifically, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.}, + pubstate = {prepublished}, + keywords = {55U35 18G30 18D10,Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/ME8UH6X7/Riehl and Verity - 2014 - The theory and practice of Reedy categories.pdf;/home/nerf/Zotero/storage/TU3Y2293/1304.html} +} + +@article{shulmanREEDYCATEGORIESTHEIR, + title = {{{REEDY CATEGORIES AND THEIR GENERALIZATIONS}}}, + author = {Shulman, Michael}, + abstract = {We observe that the Reedy model structure on a diagram category can be constructed by iterating an operation of “bigluing” model structures along a pair of functors and a natural transformation. This yields a new explanation of the definition of Reedy categories: they are almost exactly those small categories for which the category of diagrams and its model structure can be constructed by iterated bigluing. It also gives a consistent way to produce generalizations of Reedy categories, including the generalized Reedy categories of Cisinski and Berger–Moerdijk and the enriched Reedy categories of Angeltveit, but also new versions such as a combined notion of “enriched generalized Reedy category”.}, + langid = {english}, + file = {/home/nerf/Zotero/storage/BMRJ6NMU/Shulman - REEDY CATEGORIES AND THEIR GENERALIZATIONS.pdf} +} + +@incollection{balchinBisimplicialSets2021, + title = {Bisimplicial {{Sets}}}, + booktitle = {A {{Handbook}} of {{Model Categories}}}, + author = {Balchin, Scott}, + editor = {Balchin, Scott}, + date = {2021}, + pages = {205--215}, + publisher = {Springer International Publishing}, + location = {Cham}, + doi = {10.1007/978-3-030-75035-0_12}, + url = {https://doi.org/10.1007/978-3-030-75035-0_12}, + urldate = {2024-04-10}, + abstract = {The category of bisimplicial sets is the functor category \$\$\textbackslash mathbf\{Set\} \textasciicircum\{(\textbackslash varDelta \textasciicircum\{op\} \textbackslash times \textbackslash varDelta \textasciicircum\{op\})\}\$\$Set(Δop×Δop), which we denote \$\$\textbackslash mathbf\{ssSet\} \$\$ssSet. Equivalently, \$\$\textbackslash mathbf\{ssSet\} \$\$ssSetis the category of simplicial objects in simplicial sets, i.e., \$\$\textbackslash mathbf\{ssSet\} \textbackslash cong \textbackslash mathbf\{sSet\} \textasciicircum\{\textbackslash varDelta \textasciicircum\{op\}\}\$\$ssSet≅sSetΔop. Under this identification, one could equally call a bisimplicial set a simplicial space.}, + isbn = {978-3-030-75035-0}, + langid = {english}, + file = {/home/nerf/Zotero/storage/3LJ3IU2J/Balchin - 2021 - Bisimplicial Sets.pdf} } @online{NCategoryCafe, @@ -673,19 +746,146 @@ file = {/home/nerf/Zotero/storage/FG4SPDSM/what_is_a_reedy_category.html} } -@unpublished{ortonAxiomsModellingCubical2018, - title = {Axioms for {{Modelling Cubical Type Theory}} in a {{Topos}}}, - author = {Orton, Ian and Pitts, Andrew M.}, - date = {2018-12-08}, - eprint = {1712.04864}, +@incollection{riehlMadetoOrderWeakFactorization2015a, + title = {Made-to-{{Order Weak Factorization Systems}}}, + booktitle = {Extended {{Abstracts Fall}} 2013}, + author = {Riehl, Emily}, + editor = {González, Maria Del Mar and Yang, Paul C. and Gambino, Nicola and Kock, Joachim}, + date = {2015}, + pages = {87--92}, + publisher = {Springer International Publishing}, + location = {Cham}, + doi = {10.1007/978-3-319-21284-5_17}, + url = {https://link.springer.com/10.1007/978-3-319-21284-5_17}, + urldate = {2024-04-15}, + isbn = {978-3-319-21283-8 978-3-319-21284-5}, + langid = {english}, + file = {/home/nerf/Zotero/storage/PN8KT9LC/Riehl - 2015 - Made-to-Order Weak Factorization Systems.pdf} +} + +@article{riehlINDUCTIVEPRESENTATIONSGENERALIZED, + title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}}, + author = {Riehl, Emily}, + abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.}, + langid = {english}, + file = {/home/nerf/Zotero/storage/2CCAMCEM/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf} +} + +@inproceedings{angiuliCartesianCubicalComputational2018, + title = {Cartesian {{Cubical Computational Type Theory}}: {{Constructive Reasoning}} with {{Paths}} and {{Equalities}}}, + shorttitle = {Cartesian {{Cubical Computational Type Theory}}}, + booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{CSL}}.2018.6}, + author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert}, + date = {2018}, + publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik}, + doi = {10.4230/LIPIcs.CSL.2018.6}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6}, + urldate = {2024-04-28}, + abstract = {We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.}, + eventtitle = {27th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2018)}, + langid = {english}, + file = {/home/nerf/Zotero/storage/XTZNK2WW/Angiuli et al. - 2018 - Cartesian Cubical Computational Type Theory Const.pdf} +} + +@article{bartonModel2CategoryEnriched2019, + title = {A {{Model}} 2-{{Category}} of {{Enriched Combinatorial Premodel Categories}}}, + author = {Barton, Reid William}, + date = {2019-09-10}, + issn = {4201-3127}, + url = {https://dash.harvard.edu/handle/1/42013127}, + urldate = {2024-04-28}, + abstract = {Quillen equivalences induce equivalences of homotopy theories and therefore form a natural choice for the "weak equivalences" between model categories. In [21], Hovey asked whether the 2-category Mod of model categories has a "model 2-category structure" with these weak equivalences. We give an example showing that Mod does not have pullbacks, so cannot be a model 2-category. We can try to repair this lack of limits by generalizing the notion of model category. The lack of limits in Mod is due to the two-out-of-three axiom, so we define a premodel category to be a complete and cocomplete category equipped with two nested weak factorization systems. Combinatorial premodel categories form a 2-category CPM with excellent algebraic properties: CPM has all limits and colimits and is equipped with a tensor product (representing Quillen bifunctors) which is adjoint to an internal Hom. The homotopy theory of a model category depends in an essential way on the weak equivalences, so it does not extend directly to premodel categories. We build a substitute homotopy theory under an additional axiom on the premodel category, which holds automatically for a premodel category enriched in a monoidal model category V. The 2-category of combinatorial V-premodel categories VCPM is simply the 2-category of modules over the monoid object V, so VCPM inherits the algebraic structure of CPM. We construct a model 2-category structure on VCPM for V a tractable symmetric monoidal model category, by adapting Szumiło's construction of a fibration category of cofibration categories [35]. For set-theoretic reasons, constructing factorizations for this model 2-category structure requires a technical variant of the small object argument which relies on an analysis of the rank of combinatoriality of a premodel category.}, + langid = {english}, + annotation = {Accepted: 2019-12-11T10:06:35Z}, + file = {/home/nerf/Zotero/storage/ALJR3L7T/Barton - 2019 - A Model 2-Category of Enriched Combinatorial Premo.pdf} +} + +@online{hoveyModelCategories2007, + title = {Model {{Categories}}}, + author = {Hovey, Mark}, + date = {2007-10-17}, + series = {Mathematical {{Surveys}} and {{Monographs}}}, + volume = {63}, + publisher = {American Mathematical Society}, + issn = {0076-5376, 2331-7159}, + doi = {10.1090/surv/063}, + url = {https://www.ams.org/surv/063}, + urldate = {2024-04-28}, + abstract = {Advancing research. Creating connections.}, + isbn = {9780821843611 9781470412906}, + langid = {english}, + organization = {American Mathematical Society} +} + +@online{coquandVariationCubicalSets2014, + title = {Variation on {{Cubical Sets}}}, + author = {Coquand, Thierry}, + date = {2014}, + url = {https://www.cse.chalmers.se/~coquand/diag.pdf}, + urldate = {2024-04-30}, + file = {/home/nerf/Zotero/storage/HQBY2TZY/diag.pdf} +} + +@article{streicherSimplicialSetsCubical2021, + title = {Simplicial Sets inside Cubical Sets}, + author = {Streicher, Thomas and Weinberger, Jonathan}, + date = {2021-03-15}, + journaltitle = {Theory and Applications of Categories}, + volume = {37}, + number = {10}, + pages = {276--286}, + url = {http://www.tac.mta.ca/tac/volumes/37/10/37-10abs.html}, + urldate = {2024-05-02}, + file = {/home/nerf/Zotero/storage/DSG2FX6B/Streicher and Weinberger - 2021 - Simplicial sets inside cubical sets.pdf} +} + +@online{riehlTypeTheorySynthetic2023, + title = {A Type Theory for Synthetic \$\textbackslash infty\$-Categories}, + author = {Riehl, Emily and Shulman, Michael}, + date = {2023-06-08}, + eprint = {1705.07442}, eprinttype = {arXiv}, - eprintclass = {cs}, - doi = {10.23638/LMCS-14(4:23)2018}, - url = {http://arxiv.org/abs/1712.04864}, - urldate = {2022-05-11}, - abstract = {The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object \$I\$ in a topos to give such a path-based model of type theory in which paths are just functions with domain \$I\$. Cohen, Coquand, Huber and M\textbackslash "ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)}, - keywords = {Computer Science - Logic in Computer Science,F.4.1}, - file = {/home/nerf/Zotero/storage/IPQSVWQ9/Orton and Pitts - 2018 - Axioms for Modelling Cubical Type Theory in a Topo.pdf;/home/nerf/Zotero/storage/KRK2SGUB/1712.html} + eprintclass = {math}, + doi = {10.48550/arXiv.1705.07442}, + url = {http://arxiv.org/abs/1705.07442}, + urldate = {2024-05-30}, + abstract = {We propose foundations for a synthetic theory of \$(\textbackslash infty,1)\$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.}, + pubstate = {prepublished}, + keywords = {03G30 18G55 55U40,Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/6MQM9TWA/Riehl and Shulman - 2023 - A type theory for synthetic $infty$-categories.pdf;/home/nerf/Zotero/storage/H3UW42V3/1705.html} +} + +@online{solution, + title = {The Equivariant Model Structure on Cartesian Cubical Sets}, + author = {Awodey, Steve and Cavallo, Evan and Coquand, Thierry and Riehl, Emily and Sattler, Christian}, + date = {2024-06-26}, + eprint = {2406.18497}, + eprinttype = {arXiv}, + eprintclass = {cs, math}, + doi = {10.48550/arXiv.2406.18497}, + url = {http://arxiv.org/abs/2406.18497}, + urldate = {2024-07-03}, + abstract = {We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.}, + pubstate = {prepublished}, + shorthand = {ACCRS}, + keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/AKJBUSV6/Awodey et al. - 2024 - The equivariant model structure on cartesian cubic.pdf;/home/nerf/Zotero/storage/ZD7WA4UC/2406.html} +} + +@online{awodeyHofmannStreicherUniverses2023, + title = {On {{Hofmann-Streicher}} Universes}, + author = {Awodey, Steve}, + date = {2023-07-11}, + eprint = {2205.10917}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.2205.10917}, + url = {http://arxiv.org/abs/2205.10917}, + urldate = {2024-07-05}, + abstract = {We have another look at the construction by Hofmann and Streicher of a universe \$(U,\{\textbackslash mathsf\{E\}l\})\$ for the interpretation of Martin-L\textbackslash "of type theory in a presheaf category \$\textbackslash psh\{\textbackslash C\}\$. It turns out that \$(U,\{\textbackslash mathsf\{E\}l\})\$ can be described as the \textbackslash emph\{categorical nerve\} of the classifier \$\textbackslash dot\{\textbackslash Set\}\textasciicircum\{\textbackslash mathsf\{op\}\} \textbackslash to \textbackslash op\{\textbackslash Set\}\$ for discrete fibrations in \$\textbackslash Cat\$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf \$P : \textbackslash op\{\textbackslash C\}\textbackslash to\textbackslash Set\$ to its category of elements \$\textbackslash int\_\textbackslash C P\$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.}, + pubstate = {prepublished}, + keywords = {Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/NIIL8ZAK/Awodey - 2023 - On Hofmann-Streicher universes.pdf;/home/nerf/Zotero/storage/J3DQ66DM/2205.html} } @article{pareAbsoluteColimits1971, @@ -704,22 +904,49 @@ file = {/home/nerf/Zotero/storage/E68DYK76/0021869371901165.html} } -@incollection{quillenAxiomaticHomotopyTheory1967, - title = {Axiomatic Homotopy Theory}, - booktitle = {Homotopical {{Algebra}}}, - author = {Quillen, Daniel G.}, - editor = {Quillen, Daniel G.}, - date = {1967}, - pages = {1--64}, - publisher = {Springer}, - location = {Berlin, Heidelberg}, - doi = {10.1007/BFb0097439}, - url = {https://doi.org/10.1007/BFb0097439}, - urldate = {2024-08-02}, - isbn = {978-3-540-35523-6}, +@online{Section00VCFunctoriality, + title = {Section 7.5 ({{00VC}}): {{Functoriality}} of Categories of Presheaves—{{The Stacks}} Project}, + url = {https://stacks.math.columbia.edu/tag/00VC}, + urldate = {2024-07-12}, + file = {/home/nerf/Zotero/storage/LEP4E2FJ/00VC.html} +} + +@inreference{stacks00VC, + title = {The {{Stacks}} Project}, + author = {The \{Stacks project authors\}}, + url = {https://stacks.math.columbia.edu/tag/00VC} +} + +@article{sattlerCYLINDRICALMODELSTRUCTURES, + title = {{{CYLINDRICAL MODEL STRUCTURES}}}, + author = {Sattler, Christian}, + url = {https://www.cse.chalmers.se/~sattler/docs/interval-model-structure.pdf}, langid = {english}, - keywords = {Double Coset,Homotopy Category,Homotopy Theory,Model Category,Weak Equivalence}, - file = {/home/nerf/Zotero/storage/WIV7ECSM/Quillen - 1967 - Axiomatic homotopy theory.pdf} + file = {/home/nerf/Zotero/storage/G9NTWNAY/Sattler - CYLINDRICAL MODEL STRUCTURES.pdf} +} + +@online{shulmanAllInftyToposes2019, + title = {All \$(\textbackslash infty,1)\$-Toposes Have Strict Univalent Universes}, + author = {Shulman, Michael}, + date = {2019-04-26}, + eprint = {1904.07004}, + eprinttype = {arXiv}, + eprintclass = {math}, + doi = {10.48550/arXiv.1904.07004}, + url = {http://arxiv.org/abs/1904.07004}, + urldate = {2024-07-23}, + abstract = {We prove the conjecture that any Grothendieck \$(\textbackslash infty,1)\$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to \$(\textbackslash infty,1)\$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.}, + pubstate = {prepublished}, + keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/STEZIS8H/Shulman - 2019 - All $(infty,1)$-toposes have strict univalent uni.pdf;/home/nerf/Zotero/storage/XZQ93HPD/1904.html} +} + +@article{riehlINDUCTIVEPRESENTATIONSGENERALIZEDa, + title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}}, + author = {Riehl, Emily}, + abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.}, + langid = {english}, + file = {/home/nerf/Zotero/storage/6G7N6N5U/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf} } @incollection{quillenExamplesSimplicialHomotopy1967, @@ -740,22 +967,22 @@ file = {/home/nerf/Zotero/storage/SV4WJESD/Quillen - 1967 - Examples of simplicial homotopy theories.pdf} } -@book{quillenHomotopicalAlgebra1967, - title = {Homotopical {{Algebra}}}, +@incollection{quillenAxiomaticHomotopyTheory1967, + title = {Axiomatic Homotopy Theory}, + booktitle = {Homotopical {{Algebra}}}, author = {Quillen, Daniel G.}, - editor = {Dold, A. and Eckmann, B.}, - editortype = {redactor}, + editor = {Quillen, Daniel G.}, date = {1967}, - series = {Lecture {{Notes}} in {{Mathematics}}}, - volume = {43}, + pages = {1--64}, publisher = {Springer}, location = {Berlin, Heidelberg}, - doi = {10.1007/BFb0097438}, - url = {http://link.springer.com/10.1007/BFb0097438}, - urldate = {2022-04-27}, - isbn = {978-3-540-03914-3 978-3-540-35523-6}, - keywords = {algebra,homotopical algebra,Homotopie,homotopy,homotopy theory,Quillen}, - file = {/home/nerf/Zotero/storage/JG33WVEZ/Quillen - 1967 - Homotopical Algebra.pdf} + doi = {10.1007/BFb0097439}, + url = {https://doi.org/10.1007/BFb0097439}, + urldate = {2024-08-02}, + isbn = {978-3-540-35523-6}, + langid = {english}, + keywords = {Double Coset,Homotopy Category,Homotopy Theory,Model Category,Weak Equivalence}, + file = {/home/nerf/Zotero/storage/WIV7ECSM/Quillen - 1967 - Axiomatic homotopy theory.pdf} } @book{quillenHomotopicalAlgebra1967a, @@ -776,292 +1003,81 @@ file = {/home/nerf/Zotero/storage/6JP38TF2/Quillen - 1967 - Homotopical Algebra.pdf} } -@unpublished{riehlAlgebraicModelStructures2011, - title = {Algebraic Model Structures}, - author = {Riehl, Emily}, - date = {2011-03-11}, - eprint = {0910.2733}, +@online{hoveyModelCategories2007a, + title = {Model {{Categories}}}, + author = {Hovey, Mark}, + date = {2007-10-17}, + series = {Mathematical {{Surveys}} and {{Monographs}}}, + volume = {63}, + publisher = {American Mathematical Society}, + issn = {0076-5376, 2331-7159}, + doi = {10.1090/surv/063}, + url = {https://www.ams.org/surv/063}, + urldate = {2024-08-02}, + abstract = {Advancing research. Creating connections.}, + isbn = {9780821843611 9781470412906}, + langid = {english}, + organization = {American Mathematical Society} +} + +@online{awodeyCartesianCubicalModel2023, + title = {Cartesian Cubical Model Categories}, + author = {Awodey, Steve}, + date = {2023-07-14}, + eprint = {2305.00893}, eprinttype = {arXiv}, eprintclass = {math}, - url = {http://arxiv.org/abs/0910.2733}, - urldate = {2022-04-26}, - abstract = {We define a new notion of an algebraic model structure, in which the cofibrations and fibrations are retracts of coalgebras for comonads and algebras for monads, and prove "algebraic" analogs of classical results. Using a modified version of Quillen's small object argument, we show that every cofibrantly generated model structure in the usual sense underlies a cofibrantly generated algebraic model structure. We show how to pass a cofibrantly generated algebraic model structure across an adjunction, and we characterize the algebraic Quillen adjunction that results. We prove that pointwise natural weak factorization systems on diagram categories are cofibrantly generated if the original ones are, and we give an algebraic generalization of the projective model structure. Finally, we prove that certain fundamental comparison maps present in any cofibrantly generated model category are cofibrations when the cofibrations are monomorphisms, a conclusion that does not seem to be provable in the classical, non-algebraic, theory.}, - keywords = {55U35 18A32,Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/7748DLXS/Riehl - 2011 - Algebraic model structures.pdf;/home/nerf/Zotero/storage/5TLYJVHI/0910.html} + doi = {10.48550/arXiv.2305.00893}, + url = {http://arxiv.org/abs/2305.00893}, + urldate = {2024-08-03}, + abstract = {The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.}, + pubstate = {prepublished}, + keywords = {18N40 18B25 18N45,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic}, + file = {/home/nerf/Zotero/storage/KWCXVX7B/Awodey - 2023 - Cartesian cubical model categories.pdf;/home/nerf/Zotero/storage/PNTHDEYX/2305.html} } -@book{riehlCategoricalHomotopyTheory2014, - title = {Categorical {{Homotopy Theory}}}, - author = {Riehl, Emily}, - date = {2014}, - series = {New {{Mathematical Monographs}}}, - publisher = {Cambridge University Press}, - location = {Cambridge}, - doi = {10.1017/CBO9781107261457}, - url = {https://www.cambridge.org/core/books/categorical-homotopy-theory/556C7A200B521E61466BB7763C49DDA4}, - urldate = {2023-07-07}, - abstract = {This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: either as derived functors definable when the appropriate diagram categories admit a compatible model structure, or through particular formulae that give the right notion in certain examples. Emily Riehl unifies these seemingly rival perspectives and demonstrates that model structures on diagram categories are irrelevant. Homotopy (co)limits are explained to be a special case of weighted (co)limits, a foundational topic in enriched category theory. In Part II, Riehl further examines this topic, separating categorical arguments from homotopical ones. Part III treats the most ubiquitous axiomatic framework for homotopy theory - Quillen's model categories. Here, Riehl simplifies familiar model categorical lemmas and definitions by focusing on weak factorization systems. Part IV introduces quasi-categories and homotopy coherence.}, - isbn = {978-1-107-04845-4}, - file = {/home/nerf/Zotero/storage/NEXTFSKD/Riehl - Categorical homotopy theory.pdf;/home/nerf/Zotero/storage/IJYSYMC6/556C7A200B521E61466BB7763C49DDA4.html} -} - -@article{riehlCategoryTheoryContext, - title = {Category Theory in Context}, - author = {Riehl, Emily}, +@article{hofmannLiftingGrothendieckUniverses1997, + title = {Lifting {{Grothendieck Universes}}}, + author = {Hofmann, Martin and Streicher, Thomas}, + date = {1997-21}, + url = {https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf}, langid = {english}, - file = {/home/nerf/Zotero/storage/4WNNYCP7/Riehl - Category theory in context.pdf} + file = {/home/nerf/Zotero/storage/LE9B8IMD/Hofmann et al. - Lifting Grothendieck Universes.pdf} } -@article{riehlINDUCTIVEPRESENTATIONSGENERALIZED, - title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}}, - author = {Riehl, Emily}, - abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.}, - langid = {english}, - file = {/home/nerf/Zotero/storage/2CCAMCEM/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf} -} - -@article{riehlINDUCTIVEPRESENTATIONSGENERALIZEDa, - title = {{{INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEGORIES}}}, - author = {Riehl, Emily}, - abstract = {This note explores the algebraic perspective on the notion of generalized Reedy category introduced by Berger and Moerdijk [BM08]. The aim is to unify inductive arguments by means of a canonical presentation of the hom bifunctor as a “generalized cell complex.” This is analogous to the weighted (co)limits approach to strict Reedy category theory presented in [RV14], which inspired this work. These presentations are used to prove that various functors associated to categories of Reedy-indexed diagrams are “derived” preserving pointwise weak equivalences between appropriately fibrant or cofibrant diagrams.}, - langid = {english}, - file = {/home/nerf/Zotero/storage/6G7N6N5U/Riehl - INDUCTIVE PRESENTATIONS OF GENERALIZED REEDY CATEG.pdf} -} - -@incollection{riehlMadetoOrderWeakFactorization2015a, - title = {Made-to-{{Order Weak Factorization Systems}}}, - booktitle = {Extended {{Abstracts Fall}} 2013}, - author = {Riehl, Emily}, - editor = {González, Maria Del Mar and Yang, Paul C. and Gambino, Nicola and Kock, Joachim}, - date = {2015}, - pages = {87--92}, - publisher = {Springer International Publishing}, - location = {Cham}, - doi = {10.1007/978-3-319-21284-5_17}, - url = {https://link.springer.com/10.1007/978-3-319-21284-5_17}, - urldate = {2024-04-15}, - isbn = {978-3-319-21283-8 978-3-319-21284-5}, - langid = {english}, - file = {/home/nerf/Zotero/storage/PN8KT9LC/Riehl - 2015 - Made-to-Order Weak Factorization Systems.pdf} -} - -@online{riehlTheoryPracticeReedy2014, - title = {The Theory and Practice of {{Reedy}} Categories}, - author = {Riehl, Emily and Verity, Dominic}, - date = {2014-06-03}, - eprint = {1304.6871}, +@article{gambinoPolynomialFunctorsPolynomial2013, + title = {Polynomial Functors and Polynomial Monads}, + author = {Gambino, Nicola and Kock, Joachim}, + date = {2013-01}, + journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society}, + shortjournal = {Math. Proc. Camb. Phil. Soc.}, + volume = {154}, + number = {1}, + eprint = {0906.4931}, eprinttype = {arXiv}, eprintclass = {math}, - doi = {10.48550/arXiv.1304.6871}, - url = {http://arxiv.org/abs/1304.6871}, - urldate = {2024-04-07}, - abstract = {The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but difficult to find in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Specifically, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.}, - pubstate = {prepublished}, - keywords = {55U35 18G30 18D10,Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/ME8UH6X7/Riehl and Verity - 2014 - The theory and practice of Reedy categories.pdf;/home/nerf/Zotero/storage/TU3Y2293/1304.html} + pages = {153--192}, + issn = {0305-0041, 1469-8064}, + doi = {10.1017/S0305004112000394}, + url = {http://arxiv.org/abs/0906.4931}, + urldate = {2024-08-04}, + abstract = {We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.}, + keywords = {18C15 18D05 18D50 03G30,Mathematics - Category Theory}, + file = {/home/nerf/Zotero/storage/JMIDZIWR/Gambino and Kock - 2013 - Polynomial functors and polynomial monads.pdf;/home/nerf/Zotero/storage/CADCALSE/0906.html} } -@article{riehlTOPOSSEMANTICSHOMOTOPY, - title = {{{ON THE}} ∞-{{TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY}}}, - author = {Riehl, Emily}, - pages = {37}, - abstract = {Many introductions to homotopy type theory and the univalence axiom neglect to explain what any of it means, glossing over the semantics of this new formal system in traditional set-based foundations. This series of talks will attempt to survey the state of the art, first presenting Voevodsky’s simplicial model of univalent foundations and then touring Shulman’s vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ∞-topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.}, +@article{lackAdhesiveQuasiadhesiveCategories2005, + title = {Adhesive and Quasiadhesive Categories}, + author = {Lack, Stephen and Sobociński, Paweł}, + date = {2005}, + journaltitle = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications}, + volume = {39}, + number = {3}, + pages = {511--545}, + issn = {1290-385X}, + doi = {10.1051/ita:2005028}, + url = {http://www.numdam.org/item/ITA_2005__39_3_511_0/}, + urldate = {2024-08-07}, langid = {english}, - file = {/home/nerf/Zotero/storage/UA9ZRJ5Y/Riehl - ON THE ∞-TOPOS SEMANTICS OF HOMOTOPY TYPE THEORY.pdf} -} - -@online{riehlTypeTheorySynthetic2023, - title = {A Type Theory for Synthetic \$\textbackslash infty\$-Categories}, - author = {Riehl, Emily and Shulman, Michael}, - date = {2023-06-08}, - eprint = {1705.07442}, - eprinttype = {arXiv}, - eprintclass = {math}, - doi = {10.48550/arXiv.1705.07442}, - url = {http://arxiv.org/abs/1705.07442}, - urldate = {2024-05-30}, - abstract = {We propose foundations for a synthetic theory of \$(\textbackslash infty,1)\$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.}, - pubstate = {prepublished}, - keywords = {03G30 18G55 55U40,Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/6MQM9TWA/Riehl and Shulman - 2023 - A type theory for synthetic $infty$-categories.pdf;/home/nerf/Zotero/storage/H3UW42V3/1705.html} -} - -@video{riehlVid, - entrysubtype = {video}, - title = {The {{Equivariant Uniform Kan Fibration Model}} of {{Cubical Homotopy Type Theory}} - {{YouTube}}}, - editor = {Riehl, Emily}, - editortype = {director}, - date = {2020-05-26}, - url = {https://www.youtube.com/watch?v=A8tEwxM7uxE}, - urldate = {2022-06-19}, - abstract = {Dr Emily Riehl Johns Hopkins University}, - file = {/home/nerf/Zotero/storage/SYCCCLDV/watch.html} -} - -@online{rileyTypeTheoryTiny2024, - title = {A {{Type Theory}} with a {{Tiny Object}}}, - author = {Riley, Mitchell}, - date = {2024-03-04}, - eprint = {2403.01939}, - eprinttype = {arXiv}, - eprintclass = {cs, math}, - doi = {10.48550/arXiv.2403.01939}, - url = {http://arxiv.org/abs/2403.01939}, - urldate = {2024-03-12}, - abstract = {We present an extension of Martin-L\textbackslash "of Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected left adjoint. We demonstrate the practicality of this type theory by proving various properties related to tininess internally and suggest a few potential applications.}, - pubstate = {prepublished}, - keywords = {Computer Science - Programming Languages,Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/DM45P9J4/Riley - 2024 - A Type Theory with a Tiny Object.pdf;/home/nerf/Zotero/storage/8KAP7SMU/2403.html} -} - -@article{sattlerCYLINDRICALMODELSTRUCTURES, - title = {{{CYLINDRICAL MODEL STRUCTURES}}}, - author = {Sattler, Christian}, - url = {https://www.cse.chalmers.se/~sattler/docs/interval-model-structure.pdf}, - langid = {english}, - file = {/home/nerf/Zotero/storage/G9NTWNAY/Sattler - CYLINDRICAL MODEL STRUCTURES.pdf} -} - -@online{sattlerEquivalenceExtensionProperty2017, - title = {The {{Equivalence Extension Property}} and {{Model Structures}}}, - author = {Sattler, Christian}, - date = {2017-04-23}, - url = {https://arxiv.org/abs/1704.06911v4}, - urldate = {2023-08-23}, - abstract = {We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex\textasciicircum infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.}, - langid = {english}, - pubstate = {prepublished}, - keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic,The unknown Paper?}, - file = {/home/nerf/Zotero/storage/GFLT3HLU/Sattler - 2017 - The Equivalence Extension Property and Model Struc.pdf;/home/nerf/Zotero/storage/FDPHZXNP/1704.html;/home/nerf/Zotero/storage/SEADD4R7/1704.html} -} - -@online{sattlerIdempotentCompletionCubes2019, - title = {Idempotent Completion of Cubes in Posets}, - author = {Sattler, Christian}, - date = {2019-03-08}, - eprint = {1805.04126}, - eprinttype = {arXiv}, - eprintclass = {math}, - doi = {10.48550/arXiv.1805.04126}, - url = {http://arxiv.org/abs/1805.04126}, - urldate = {2023-08-23}, - abstract = {This note concerns the category \$\textbackslash Box\$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects \$[1]\textasciicircum n\$ with \$n \textbackslash geq 0\$. We show that the idempotent completion of \$\textbackslash Box\$ consists of finite complete posets. It follows that cubical sets, ie presheaves over \$\textbackslash Box\$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.}, - pubstate = {prepublished}, - keywords = {Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/SYH7C9JV/Sattler - 2019 - Idempotent completion of cubes in posets.pdf;/home/nerf/Zotero/storage/9ZN8RBCZ/1805.html} -} - -@online{Section00VCFunctoriality, - title = {Section 7.5 ({{00VC}}): {{Functoriality}} of Categories of Presheaves—{{The Stacks}} Project}, - url = {https://stacks.math.columbia.edu/tag/00VC}, - urldate = {2024-07-12}, - file = {/home/nerf/Zotero/storage/LEP4E2FJ/00VC.html} -} - -@online{shulmanAllInftyToposes2019, - title = {All \$(\textbackslash infty,1)\$-Toposes Have Strict Univalent Universes}, - author = {Shulman, Michael}, - date = {2019-04-26}, - eprint = {1904.07004}, - eprinttype = {arXiv}, - eprintclass = {math}, - doi = {10.48550/arXiv.1904.07004}, - url = {http://arxiv.org/abs/1904.07004}, - urldate = {2024-07-23}, - abstract = {We prove the conjecture that any Grothendieck \$(\textbackslash infty,1)\$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to \$(\textbackslash infty,1)\$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.}, - pubstate = {prepublished}, - keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory}, - file = {/home/nerf/Zotero/storage/STEZIS8H/Shulman - 2019 - All $(infty,1)$-toposes have strict univalent uni.pdf;/home/nerf/Zotero/storage/XZQ93HPD/1904.html} -} - -@article{shulmanREEDYCATEGORIESTHEIR, - title = {{{REEDY CATEGORIES AND THEIR GENERALIZATIONS}}}, - author = {Shulman, Michael}, - abstract = {We observe that the Reedy model structure on a diagram category can be constructed by iterating an operation of “bigluing” model structures along a pair of functors and a natural transformation. This yields a new explanation of the definition of Reedy categories: they are almost exactly those small categories for which the category of diagrams and its model structure can be constructed by iterated bigluing. It also gives a consistent way to produce generalizations of Reedy categories, including the generalized Reedy categories of Cisinski and Berger–Moerdijk and the enriched Reedy categories of Angeltveit, but also new versions such as a combined notion of “enriched generalized Reedy category”.}, - langid = {english}, - file = {/home/nerf/Zotero/storage/BMRJ6NMU/Shulman - REEDY CATEGORIES AND THEIR GENERALIZATIONS.pdf} -} - -@online{solution, - title = {The Equivariant Model Structure on Cartesian Cubical Sets}, - author = {Awodey, Steve and Cavallo, Evan and Coquand, Thierry and Riehl, Emily and Sattler, Christian}, - date = {2024-06-26}, - eprint = {2406.18497}, - eprinttype = {arXiv}, - eprintclass = {cs, math}, - doi = {10.48550/arXiv.2406.18497}, - url = {http://arxiv.org/abs/2406.18497}, - urldate = {2024-07-03}, - abstract = {We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.}, - pubstate = {prepublished}, - shorthand = {ACCRS}, - keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/AKJBUSV6/Awodey et al. - 2024 - The equivariant model structure on cartesian cubic.pdf;/home/nerf/Zotero/storage/ZD7WA4UC/2406.html} -} - -@inreference{stacks00VC, - title = {The {{Stacks}} Project}, - author = {The \{Stacks project authors\}}, - url = {https://stacks.math.columbia.edu/tag/00VC} -} - -@book{streicherSemanticsTypeTheory1991, - title = {Semantics of {{Type Theory}}}, - author = {Streicher, Thomas}, - date = {1991}, - publisher = {Birkhäuser Boston}, - location = {Boston, MA}, - doi = {10.1007/978-1-4612-0433-6}, - url = {http://link.springer.com/10.1007/978-1-4612-0433-6}, - urldate = {2023-09-02}, - isbn = {978-1-4612-6757-7 978-1-4612-0433-6}, - langid = {english}, - file = {/home/nerf/Zotero/storage/ALA3AMGY/Streicher - 1991 - Semantics of Type Theory.pdf} -} - -@article{streicherSimplicialSetsCubical2021, - title = {Simplicial Sets inside Cubical Sets}, - author = {Streicher, Thomas and Weinberger, Jonathan}, - date = {2021-03-15}, - journaltitle = {Theory and Applications of Categories}, - volume = {37}, - number = {10}, - pages = {276--286}, - url = {http://www.tac.mta.ca/tac/volumes/37/10/37-10abs.html}, - urldate = {2024-05-02}, - file = {/home/nerf/Zotero/storage/DSG2FX6B/Streicher and Weinberger - 2021 - Simplicial sets inside cubical sets.pdf} -} - -@incollection{streicherUNIVERSESTOPOSES2005, - title = {{{UNIVERSES IN TOPOSES}}}, - booktitle = {From {{Sets}} and {{Types}} to {{Topology}} and {{Analysis}}}, - author = {Streicher, Thomas}, - editor = {Crosilla, Laura and Schuster, Peter}, - date = {2005-10-06}, - edition = {1}, - pages = {78--90}, - publisher = {Oxford University PressOxford}, - doi = {10.1093/acprof:oso/9780198566519.003.0005}, - url = {https://academic.oup.com/book/5354/chapter/148144921}, - urldate = {2023-11-14}, - abstract = {We discuss a notion of universe in toposes which from a logical point of view gives rise to an extension of Higher Order Intuitionistic Arithmetic (HAH) that allows one to construct families of types in such a universe by structural recursion and to quantify over such families. Further, we show that (hierarchies of) such universes do exist in all sheaf and realizability toposes but neither in the free topos nor in the Vω+ω model of Zermelo set theory.}, - isbn = {978-0-19-856651-9 978-0-19-171392-7}, - langid = {english}, - file = {/home/nerf/Zotero/storage/CB5TH6EV/Streicher - 2005 - UNIVERSES IN TOPOSES.pdf} -} - -@online{swanDefinableNondefinableNotions2022, - title = {Definable and {{Non-definable Notions}} of {{Structure}}}, - author = {Swan, Andrew W.}, - date = {2022-06-27}, - eprint = {2206.13643}, - eprinttype = {arXiv}, - eprintclass = {cs, math}, - doi = {10.48550/arXiv.2206.13643}, - url = {http://arxiv.org/abs/2206.13643}, - urldate = {2024-03-11}, - abstract = {Definability is a key notion in the theory of Grothendieck fibrations that characterises when an external property of objects can be accessed from within the internal logic of the base of a fibration. In this paper we consider a generalisation of definability from properties of objects to structures on objects, introduced by Shulman under the name local representability. We first develop some general theory and show how to recover existing notions due to B\textbackslash '\{e\}nabou and Johnstone as special cases. We give several examples of definable and non definable notions o structure, focusing on algebraic weak factorisation systems, which can be naturally viewed as notions of structure on codomain fibrations. Regarding definability, we give a sufficient criterion for cofibrantly generated awfs's to be definable, generalising a construction of the universe for cubical sets, but also including some very different looking examples that do not satisfy tininess in the internal sense, that exponential functors have a right adjoint. Our examples of non definability include the identification of logical principles holding for the interval objects in simplicial sets and Bezem-Coquand-Huber cubical sets that suffice to show a certain definition of Kan fibration is not definable.}, - pubstate = {prepublished}, - keywords = {03G30 18N40,Computer Science - Logic in Computer Science,Mathematics - Category Theory,Mathematics - Logic}, - file = {/home/nerf/Zotero/storage/CJRDB5DU/Swan - 2022 - Definable and Non-definable Notions of Structure.pdf;/home/nerf/Zotero/storage/DS7C3TKZ/2206.html} + file = {/home/nerf/Zotero/storage/Y3K26BM6/Lack and Sobociński - 2005 - Adhesive and quasiadhesive categories.pdf} }