LaTeX, 40 pages. Uses Paul Taylor's diagrams, Peter Kabal's texdraw, and one eps figure. Does not compile with pdflatex. Version v3: expository improvements, more details on the Moore loop space example. 44 pages. Final version to appear in IMRN
There are a dozen definitions of weak higher categories, all of which loosen the notion of composition of arrows. A new approach is presented here, where instead the notion of identity arrow is weakened -- these are tentatively called fair categories. The approach is simplicial in spirit, but the usual simplicial category $Δ$ is replaced by a certain `fat' delta of `coloured ordinals', where the degeneracy maps are only up to homotopy. The first part of this exposition is aimed at a broad mathematical readership and contains also a brief introduction to simplicial viewpoints on higher categories in general. It is explained how the definition of fair $n$-category is almost forced upon us by three standard ideas.
The second part states some basic results about fair categories, and give examples. The category of fair 2-categories is shown to be equivalent to the category of bicategories with strict composition law. Fair 3-categories correspond to tricategories with strict composition laws. The main motivation for the theory is Simpson's weak-unit conjecture according to which $n$-groupoids with strict composition laws and weak units should model all homotopy $n$-types. A proof of a version of this conjecture in dimension 3 is announced, obtained in joint work with A. Joyal. Technical details and a fuller treatment of the applications will appear elsewhere.
We introduce twisted arrow categories of operads and of algebras over operads. Up to equivalence of categories, the simplex category $Δ$, Segal's category $Γ$, Connes cyclic category $Λ$, Moerdijk-Weiss dendroidal category $Ω$, and categories similar to graphical categories of Hackney-Robertson-Yau are twisted arrow categories of symmetric or cyclic operads. Twisted arrow categories of operads admit Segal presheaves and 2-Segal presheaves, or decomposition spaces. Twisted arrow category of an operad $P$ is the $(\infty, 1)$-localization of the corresponding category $Ω/P$ by the boundary prese…
Given an $\infty$-bicategory $\mathbb{D}$ with underlying $\infty$-category $\mathcal{D}$, we construct a Cartesian fibration $\operatorname{Tw}(\mathbb{D})\to \mathcal{D} \times \mathcal{D}^{\operatorname{op}}$, which we call the enhanced twisted arrow $\infty$-category, classifying the restricted mapping category functor $\operatorname{Map}_{\mathbb{D}}:\mathcal{D}^{\operatorname{op}}\times \mathcal{D} \to \mathbb{D}^{\operatorname{op}} \times \mathbb{D} \to \operatorname{Cat}_{\infty}$. With the aid of this new construction, we provide a description of the $\infty$-category of natural trans…
We present an abstract, categorical formulation of dependent functions in a fundamental manner and independently from the Sigma-construction. For that, we define first the notion of a category with family-arrows, or a $\f$-category. A $(\f, Σ)$-category is a $\f$-category with Sigma-objects, where a $(\f, Σ)$-category with a terminal object is exactly a type-category of Pitts, or a category with attributes of Cartmell. We introduce categories with dependent arrows, or $\di$-categories, and we show that every $(\f, Σ)$-category is a $\di$-category in a canonical way. The notion of a Sigma-objec…
A folklore result in category theory is that a (weakly) Cartesian closed category with finite co-products is distributive. Usually, the proof of this small result is carried on using the fact that the exponential functor is right adjoint to the product functor. And, since functors having a right adjoint preserve co-limits, the result follows immediately. But, when we try to explicitly construct the arrows, things become a bit more involved. In rare cases, it is pretty useful to have the exact arrows that make this isomorphism to hold. The purpose of this note is to develop the explicit proof w…
We develop a localisation theory for certain categories, yielding a 3-arrow calculus: Every morphism in the localisation is represented by a diagram of length 3, and two such diagrams represent the same morphism if and only if they can be embedded in a 3-by-3 diagram in an appropriate way. The methods to construct this localisation are similar to the Ore localisation for a 2-arrow calculus; in particular, we do not have to use zigzags of arbitrary length. Applications include the localisation of an arbitrary model category with respect to its weak equivalences as well as the localisation of it…
Grandis's non-abelian homological algebra generalizes standard homological algebra in abelian categories to \textit{homological categories}, which are a broader class of categories including for example the category of lattices and Galois connections. Here, we prove that if $\mathsf{C}$ is any category with an ideal of null morphisms with respect to which (co)kernels exist, then the arrow category of $\mathsf{C}$ is a homological category. This broadens the applicability of Grandis's framework substantially. In particular, one can form the homology of chain complexes in $\mathsf{C}$ by taking …
A certain amount of category theory is developed in an arbitrary finitely complete category with a factorization system on it, playing the role of the comprehensive factorization system on Cat. Those aspects related to the concepts of finality (in particular terminal objects), discreteness and components, representability, colimits and universal arrows, seem to be best expressed in this very general setting. Furthermore, at this level we are in fact doing not only (E,M)-category theory but, in a sense, also (E,M)-topology. Other axioms, regarding power objects, duality, exponentials and the ar…
We introduce a tensor product for symmetric monoidal categories with the following properties. Let SMC denote the 2-category with objects small symmetric monoidal categories, arrows symmetric monoidal functors and 2-cells monoidal natural transformations. Our tensor product together with a suitable unit is part of a structure on SMC that is a 2-categorical version of the symmetric monoidal closed categories. This structure is surprisingly simple. In particular the arrows involved in the associativity and symmetry laws for the tensor and in the unit cancellation laws are 2-natural and satisfy c…
When formalizing mathematics in (generalized predicative) constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family $F$ of setoids. The objects of the categories are the index setoid $I$ of the family, whereas the definition of arrows differs. The first category has for arrows triples $(a,b,f:F(a) \to F(b))$ where $…
We firstly prove the completeness of the category of crossed modules in a modified category of interest. Afterwards, we define pullback crossed modules and pullback cat$^1$-objects that are both obtained by pullback diagrams with extra structures on certain arrows. These constructions unify many corresponding results for the cases of groups, commutative algebras and can also be adapted to various algebraic structures.
This article studies the categorical setting of Abramsky, Haghverdi, and Scott's untyped linear combinatory algebras, and relates this to more recent work of Abramsky and Heunen on Frobenius algebras in the infinitary setting. The key to this is extensional reflexivity (the property of an object being isomorphic to its own internal hom. $N\cong [N\rightarrow N]$). We characterise extensional reflexivity in compact closed categories, and consider how this may be `strictified' to give monoidally equivalent categories where the isomorphisms exhibiting reflexivity are identity arrows. This results…
Batanin and Markl's operadic categories are categories in which each map is endowed with a finite collection of "abstract fibres" -- also objects of the same category -- subject to suitable axioms. We give a reconstruction of the data and axioms of operadic categories in terms of the décalage comonad D on small categories. A simple case involves unary operadic categories -- ones wherein each map has exactly one abstract fibre -- which are exhibited as categories which are, first of all, coalgebras for the comonad D, and, furthermore, algebras for the monad induced on the category of D-coalgebr…
We define the notion of an indexed profunctor over a 2-category, and use it to develop an abstract theory of limits. The theory subsumes (conical) limits, weighted limits, ends and Kan extensions. Results include an abstract version of the theorem that right adjoint functors preserve limits, and an abstract account of the phenomenon that the comparison arrow implicated in the preservation of a limit by a functor is natural in any functorial variable the functor happens to depend on. These results make an extensive use of the data and axioms of an indexed profunctor over a 2-category.
Following Lawvere's description of metric spaces using enriched category theory, we introduce a change in the base of enrichment that allows description of some aspects of (relativistic) causal spaces. All such spaces are Cauchy complete, in the sense of enriched category theory. Furthermore, we give sufficient conditions on a base monoidal category for which enriched categories are Cauchy complete if and only if their underlying categories are (their idempotent arrows split).
We prove, without set theoretic assumptions, that every locally presentable category C endowed with a tractable cofibrantly generated class of cofibrations has a unique minimal (or left induced) Quillen model structure. More generally, for any set S of arrows in C we construct the minimal model structure on C with the prescribed cofibrations and making all the arrows of S weak equivalences. We describe its class of equivalences as the "smallest Cisinski localizer containing S". Our proof rely on a careful use of the fat small object argument and J.~Lurie's "good colimits" technology and on the…
We show that the strict 1-category $\square$ of cubes -- defined to be the full subcategory of strict $ω$-categories whose objects are the Gray tensor powers of the arrow category -- are dense in the $(\infty,1)$-category $\mathsf{Cat}_ω$ of weak $(\infty,\infty)$-categories, in both Rezk-complete and incomplete variants. More precisely, we show that Joyal's category $Θ$ is contained in the idempotent completion of $\square$, and in fact that the idempotent completion of $\square$ is closed under suspensions and wedge sums. This result extends a theorem of Campbell and Maehara in dimension 2. …
It is proved that equalities between arrows assumed for cartesian categories are maximal in the sense that extending them with any new equality in the language of free cartesian categories collapses a cartesian category into a preorder. An analogous result holds for categories with binary products, which may lack a terminal object. The proof is based on a coherence result for cartesian categories, which is related to model-theoretical methods of normalization.
We define a homotopy relation between arrows of a category with weak equivalences, and give a condition under which the quotient by the homotopy relation yields the homotopy category. In the case of the fibrant-cofibrant objects of a model category this condition holds, and we show that our notion of homotopy coincides with the classical one. We also show that Quillen's construction of the homotopy category of a model category, in which the arrows are homotopical classes of a single arrow between fibrant-cofibrant objects, can be made as well for categories with weak equivalences using this no…
Quantum categories have been recently studied because of their relation to bialgebroids, small categories, and skew monoidales. This is the first of a series of papers based on the author's PhD thesis in which we examine the theory of quantum categories developed by Day, Lack, and Street. A quantum category is an opmonoidal monad on the monoidale associated to a biduality $R\dashv R^{\circ}$, or enveloping monoidale, in a monoidal bicategory of modules $\mathsf{Mod}(\mathcal{V})$ for a monoidal category $\mathcal{V}$. Lack and Street proved that quantum categories are in equivalence with right…
This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Lof type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper pla…
We construct a category, $Ω$, of which the objects are pointed categories and the arrows are pointed correspondences. The notion of a "spec datum" is introduced, as a certain relation between categories, of which one has been given a Grothendieck topology. A "geometry" is interpreted as a sub-category of $Ω$, and a formalism is given by which such a subcategory is to be associated to a spec datum, reflecting the standard construction of the category of schemes from the category of rings by affine charts.
A concrete computation -- twelve slidings with sixteen tiles -- reveals that certain commutativity phenomena occur in every double semigroup. This can be seen as a sort of Eckmann-Hilton argument, but it does not use units. The result implies in particular that all cancellative double semigroups and all inverse double semigroups are commutative. Stepping up one dimension, the result is used to prove that all strictly associative two-fold monoidal categories (with weak units) are degenerate symmetric. In particular, strictly associative one-object, one-arrow 3-groupoids (with weak units) cannot…
The familiar construction of categories of fractions, due to Gabriel and Zisman, allows one to invert a class W of arrows in a category in a universal way. Similarly, bicategories of fractions allow one to invert a collection of arrows in a bicategory. In this case the arrows are inverted in the sense that they are made into equivalences. As with categories of fractions, bicategories of fractions suffer from the defect that they need not be locally small even when the bicategory in which W lives is locally small. Similarly, in the case where W is a class of arrows in a 2-category, the bicatego…
This paper introduces the notion of a categorical pair, a pair of categories (C,C') such that every morphism in C is an object in C'. Categorical pairs are precursors to 2-categories. Arrows in C' can express relationships among the morphisms of C. In particular we show that by using a model of the linguistic process of naming, we can ensure that every morphism in C has an indirect self-reference of the form a -----> Fa where this arrow occurs in the category C'. This result is shown to generalize and clarify known fixed point theorems in logic and categories, and is applied to Goedel's Incomp…
From the Bayesian perspective, the category of conditional probabilities (a variant of the Kleisli category of the Giry monad, whose objects are measurable spaces and arrows are Markov kernels) gives a nice framework for conceptualization and analysis of many aspects of machine learning. Using categorical methods, we construct models for parametric and nonparametric Bayesian reasoning on function spaces, thus providing a basis for the supervised learning problem. In particular, stochastic processes are arrows to these function spaces which serve as prior probabilities. The resulting inference …
In 1966, John Isbell introduced a construction on categories which he termed the "couple category" but which has since come to be known as the Isbell envelope. The Isbell envelope, which combines the ideas of contravariant and covariant presheaves, has found applications in category theory, logic, and differential geometry. We clarify its meaning by exhibiting the assignation sending a locally small category to its Isbell envelope as the action on objects of a pseudomonad on the 2-category of locally small categories; this is the Isbell monad of the title. We characterise the pseudoalgebras of…
Most often, in a categorical semantics for a programming language, the substitution of terms is expressed by composition and finite products. However this does not deal with the order of evaluation of arguments, which may have major consequences when there are side-effects. In this paper Cartesian effect categories are introduced for solving this issue, and they are compared with strong monads, Freyd-categories and Haskell's Arrows. It is proved that a Cartesian effect category is a Freyd-category where the premonoidal structure is provided by a kind of binary product, called the sequential pr…
The notion of proof-net category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit free fragment of the notion of star-autonomous categ…
There exists a dispute in philosophy, going back at least to Leibniz, whether is it possible to view the world as a network of relations and relations between relations with the role of objects, between which these relations hold, entirely eliminated. Category theory seems to be the correct mathematical theory for clarifying conceptual possibilities in this respect. In this theory, objects acquire their identity either by definition, when in defining category we postulate the existence of objects, or formally by the existence of identity morphisms. We show that it is perfectly possible to get …
The aim of this article is to better understand the correspondence between $n$-cubic extensions and $3^n$-diagrams, which may be seen as non-abelian Yoneda extensions, useful in (co)homology of non-abelian algebraic structures. We study a higher-dimensional version of the coequaliser/kernel pair adjunction, which relates $n$-fold reflexive graphs with $n$-fold arrows in any exact Mal'tsev category. We first ask ourselves how this adjunction restricts to an equivalence of categories. This leads to the concept of an effective $n$-fold equivalence relation, corresponding to the $n$-fold regular e…
Cartesian differential categories were introduced to provide an abstract axiomatization of categories of differentiable functions. The fundamental example is the category whose objects are Euclidean spaces and whose arrows are smooth maps. Tensor differential categories provide the framework for categorical models of differential linear logic. The coKleisli category of any tensor differential category is always a Cartesian differential category. Cartesian differential categories, besides arising in this manner as coKleisli categories, occur in many different and quite independent ways. Thus, i…
Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It is found that with the simplest understanding of coherence this is the best on…
Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-Lof's rules for the identity types which has been considered by Cohen, Coquand, Huber and Mortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category o…
In this note we consider partial model categories, by which we mean relative categories that satisfy a weakened version of the model category axioms involving only the weak equivalences. More precisely, a partial model category will be a relative category that has the two out of six property and admits a 3-arrow calculus. We then show that Charles Rezk's result that the simplicial space obtained from a simplicial model category by taking a Reedy fibrant replacement of its simplicial nerve is a complete Segal space also holds for these partial model categories. We also note that conversely ever…
Given a 2-category $\mathcal{A}$, a $2$-functor $\mathcal{A} \overset {F} {\longrightarrow} \mathcal{C}at$ and a distinguished 1-subcategory $Σ\subset \mathcal{A}$ containing all the objects, a $σ$-cone for $F$ (with respect to $Σ$) is a lax cone such that the structural $2$-cells corresponding to the arrows of $Σ$ are invertible. The conical $σ$-limit is the universal (up to isomorphism) $σ$-cone. The notion of $σ$-limit generalises the well known notions of pseudo and lax limit. We consider the fundamental notion of $σ$-filtered} pair $(\mathcal{A}, \, Σ)$ which generalises the notion of 2-f…
Let C and D be quasi-categories (a.k.a. infinity-categories). Suppose also that one has an assignment sending commutative diagrams of C to commutative diagrams of D which respects face maps, but not necessarily degeneracy maps. (This is akin to having an assignment which respects all compositions, but may not send identity morphisms to identity morphisms.) When does this assignment give rise to an actual functor? We show that if the original assignment can be shown to respect identity morphisms up to homotopy, then there exists an honest functor of infinity-categories which respects the origin…
A partial combinatory algebra (PCA) is a set equipped with a partial binary operation that models a notion of computability. This paper studies a generalization of PCAs, introduced by W. Stekelenburg, where a PCA is not a set but an object in a given regular category. The corresponding class of categories of assemblies is closed both under taking small products and under slicing, which is to be contrasted with the situation for ordinary PCAs. We describe these two constructions explicitly at the level of PCAs, allowing us to compute a number of examples of products and slices of PCAs. Moreover…
Effective Burnside $\infty$-categories are the centerpiece of the $\infty$-categorical approach to equivariant stable homotopy theory. In this étude, we recall the construction of the twisted arrow $\infty$-category, and we give a new proof that it is an $\infty$-category, using an extremely helpful modification of an argument due to Joyal--Tierney. The twisted arrow $\infty$-category is in turn used to construct the effective Burnside $\infty$-category. We employ a variation on this theme to construct a fibrewise effective Burnside $\infty$-category. To show that this constuctionworks fibrewi…
We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
We study the *homotopy theory* of $\infty$-categories enriched in the $\infty$-category $sS$ of simplicial spaces. That is, we consider $sS$-enriched $\infty$-categories as presentations of ordinary $\infty$-categories by means of a "local" geometric realization functor $Cat_{sS} \to Cat_\infty$, and we prove that their homotopy theory presents the $\infty$-category of $\infty$-categories, i.e. that this functor induces an equivalence $Cat_{sS} [[ W_{DK}^{-1} ]] \xrightarrow{\sim} Cat_\infty$ from a localization of the $\infty$-category of $sS$-enriched $\infty$-categories. Following Dwyer--Ka…
We define involution algebroids which generalise Lie algebroids to the abstract setting of tangent categories. As a part of this generalisation the Jacobi identity which appears in classical Lie theory is replaced by an identity similar to the Yang-Baxter equation. Every classical Lie algebroid has the structure of an involution algebroid and every involution algebroid in a tangent category admits a Lie bracket on the sections of its underlying bundle. As an illustrative application we take the first steps in developing the homotopy theory of involution algebroids.
It has been known that categorical interpretations of dependent type theory with Sigma- and Id-types induce weak factorization systems. When one has a weak factorization system (L, R) on a category C in hand, it is then natural to ask whether or not (L, R) harbors an interpretation of dependent type theory with Sigma- and Id- (and possibly Pi-) types. Using the framework of display map categories to phrase this question more precisely, one would ask whether or not there exists a class D of morphisms of C such that the retract closure of D is the class R and the pair (C, D) forms a display map …
In [Homotopical Algebra, Springer LNM 43] Quillen introduces the notion of a model category: a category $\mathcal{C}$ provided with three distinguished classes of maps $\{\mathcal{W},\, \mathcal{F},\, co\mathcal{F}\}$ (weak equivalences, fibrations, cofibrations), and gives a construction of the localization $\mathcal{C}[\mathcal{W}^{-1}]$ as the quotient of $\mathcal{C}$ by the congruence relation determined by the homotopies on the sets of arrows $\mathcal{C}(X,\,Y)$. We develop here the 2-categorical localization, in which the 2-cells of this 2-localization are given by homotopies, and one …
We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond to trihomomorphisms from a bicategory into Bicat. We describe the Grothendieck construction for each kind of fibration and present a few examples of each. Fibrations in our sense, between bicategories, are closed under composition and are stable under equiv-comma. The free such fibration on a homomorphism is obtained by taking an oplax comma along an identity.