arXiv subjects

Daniel Almeida

Publications and source records attributed to Daniel Almeida.

3 recordsLinked to original sources

arXiv2026

A categorical model structure for generalized algebraic theories

We describe a (combinatorial, monoidal, Cat-enriched) Quillen model structure on the category of Cartmell's generalized algebraic theories (gats); its homotopy bicategory consists essentially of Taylor's rooted display map categories. This allows us to compare two kinds of morphisms of gats: one where sort dependency and substitution are preserved strictly, thus directly matching the syntax, and one where the given structure is preserved up to isomorphism. We prove a strictification result for morphisms out of cofibrant theories, which are the retracts of theories without sort equality axioms. Along the way, we give a structural characterization of when a contextual category can be presented without sort equality axioms. Our results also imply that when restricted to cofibrant objects, the tensor product of gats has the expected semantic behaviour, namely, it corresponds to the tensor product of locally finitely presentable categories equipped with a cofibrantly generated weak factorization system. Strict and weak morphisms specialize, respectively, to two familiar concepts of model of a gat A: ones valued in iterated families of sets, with substitution interpreted as reindexing, and set-valued models of the contextual category C(A) viewed as a finite-limit sketch. We characterize strictifiability of a model of the latter kind via a loop freeness condition on a certain map of functors out of the category of context projections of A.

math.CT↗

arXiv2026

A monoidal category of dependently sorted algebraic theories II: categorical aspects

This is the second of a pair of papers where we construct and investigate a closed monoidal structure on the category of generalized algebraic theories (in the sense of Cartmell). Having presented the tensor product of theories in a syntactic way, we now study the same structure from the perspective of contextual categories. We define the exponential $\mathcal A^\mathcal B$ between two contextual categories $\mathcal A$, $\mathcal B$, and show how this yields, as a particular case, a cotensor $\mathcal A^B$ by a small category $B$. We also introduce a concept of multimorphism $(\mathcal A_1, ..., \mathcal A_n) \rightarrow \mathcal B$ for contextual categories $\mathcal A_i$, $\mathcal B$, and describe a bijective correspondence between bimorphisms $(\mathcal A, \mathcal B) \rightarrow \mathcal C$ and morphisms $\mathcal A \rightarrow \mathcal C^\mathcal B$. We give an abstract proof that there exists a contextual category $\mathcal A \otimes \mathcal B$ such that bimorphisms $(\mathcal A, \mathcal B) \rightarrow \mathcal C$ are in natural bijection with morphisms $\mathcal A \otimes \mathcal B \rightarrow \mathcal C$. We extend $\otimes:\text{Cont} \times \text{Cont} \rightarrow \text{Cont}$ into a closed symmetric monoidal structure and give a description of certain pushout-tensor maps that, in particular, allows us to prove that the tensor product of theories from part I is functorial and presents the one constructed here.

math.CT↗

arXiv2025

A monoidal category of dependently sorted algebraic theories I: syntax

This is the first of a pair of papers where we construct and investigate a closed monoidal structure on the category of generalized algebraic theories (in the sense of Cartmell). In the present text, as a starting point, we define the tensor product, $A \otimes B$, between two generalized algebraic theories $A$ and $B$. This is done syntactically via an algorithm that uses the axioms of $A$ and $B$ in a recursive manner to produce those of $A \otimes B$. We provide examples of known structures that are recovered by our construction, such as tensor products of Lawvere theories, "cellular" products of dependent type signatures, and theories of diagrams and of displayed structures. It will be verified in the second volume that, as suggested by these special cases, the category of family-valued models $\text{Mod}(A \otimes B,\text{Fam})$ is isomorphic to $\text{Mod}(A,\textbf{Mod}(B))$ and to $\text{Mod}(B,\textbf{Mod}(A))$ for certain contextual categories $\textbf{Mod}(A)$ and $\textbf{Mod}(B)$ whose underlying categories are equivalent to $\text{Mod}(A,\text{Fam})$ and to $\text{Mod}(B,\text{Fam})$, respectively. Moreover, the cellular structure of the tensor product is obtained by combining, via a pushout-product operation, those of the two theories. We also construct a functor $\otimes_{A,B}:\mathcal C(A) \times \mathcal C(B) \rightarrow \mathcal C(A \otimes B)$ comparing the associated contextual categories, and describe isomorphisms of the forms $(A \otimes B) \otimes C \cong A \otimes (B \otimes C)$ and $A \otimes B \cong B \otimes A$. In the sequel paper we will describe a universal property of $\otimes_{A,B}$, which will induce functoriality of the tensor product and thus allow us to check the monoidal category conditions.

math.CT↗