Related papers: Semantics of multimodal adjoint type theory
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode…
We present the notion of "cyclic double multicategory", as a structure in which to organise multivariable adjunctions and mates. The classic example of a 2-variable adjunction is the hom/tensor/cotensor trio of functors; we generalise this…
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means…
We introduce a new categorical framework for studying derived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories are the objects of a double category…
Category theory has foundational importance because it provides conceptual lenses to characterize what is important in mathematics. Originally the main lenses were universal mapping properties and natural transformations. In recent decades,…
We study lax functors between bicategories as a generalized concept of monads and describe generalized notions and theorems of formal monad theory for lax functors. Our first approach is to use the 2-monad whose lax algebras are lax…
Voevodsky's derived category of motives is the main arena today for the study of algebraic cycles and motivic cohomology. In this paper we study whether the inclusions of three important subcategories of motives have a left or right…
We are checking the closed categories beginning with the category of sets and ending with the category of categories. The novelty is a generalizing the notion of adjoint functors to the joint pair of functors in the category of directed…
Given a right adjoint functor between triangulated categories and an object in the target category, we show that the unit map of adjunction on that object is a split monomorphism if and only if the object belongs to the additive closure of…
There is some consensus among orthodox category theorists that the concept of adjoint functors is the most important concept contributed to mathematics by category theory. We give a heterodox treatment of adjoints using heteromorphisms…
The structure of the category of matroids and strong maps is investigated: it has coproducts and equalizers, but not products or coequalizers; there are functors from the categories of graphs and vector spaces, the latter being faithful;…
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract…
The question "What is category theory" is approached by focusing on universal mapping properties and adjoint functors. Category theory organizes mathematics using morphisms that transmit structure and determination. Structures of…
In this work, we investigate an effective method for showing that functors between categories are left adjoints. The method applies to a large class of categories, namely locally finitely presentable categories, which are ubiquitous in…
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this…
The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural…
We construct generalized multicategories associated to an arbitrary operad in Cat that is $\Sigma$-free. The construction generalizes the passage to symmetric multicategories from permutative categories, which is the case when the operad is…
We develop a theory of adjunctions in semigroup categories, i.e. monoidal categories without a unit object. We show that a rigid semigroup category is promonoidal, and thus one can naturally adjoin a unit object to it. This extends the…
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding…
For our purposes, two functors {\Lambda} and {\Gamma} are said to be respectively left and right adjoints of each other if for any digraphs G and H, there exists a homomorphism of {\Lambda}(G) to H if and only if there exists a homomorphism…