Related papers: C-system of a module over a $Jf$-relative monad
This is the second paper in a series that aims to provide mathematical descriptions of objects and constructions related to the first few steps of the semantical theory of dependent type systems. We construct for any pair $(R,LM)$, where…
In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor $Jf:F\rightarrow Sets$ where $F$ is the category with the set of objects…
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization ready" with the emphasis on the possibility of formalization both in type theory and in constructive set…
For a finite tensor category $\mathcal C$ and a Hopf monad $T:\mathcal C\to \mathcal C$ satisfying certain conditions we describe exact indecomposable left $\mathcal C^T$-module categories in terms of left $\mathcal C$-module categories and…
Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of left modules ("Linear" natural transformations) captures an important…
For a nice-enough category $\mathcal{C}$, we construct both the morphism category ${\rm H}(\mathcal{C})$ of $\mathcal{C}$ and the category ${\rm mod}\mbox{-}\mathcal{C}$ of all finitely presented contravariant additive functors over…
Let $B$ be a bialgebra, and $A$ a left $B$-comodule algebra in a braided monoidal category $\Cc$, and assume that $A$ is also a coalgebra, with a not-necessarily associative or unital left $B$-action. Then we can define a right $A$-action…
In the theory of coalgebras $C$ over a ring $R$, the rational functor relates the category of modules over the algebra $C^*$ (with convolution product) with the category of comodules over $C$. It is based on the pairing of the algebra $C^*$…
In this article we present a solution to a conjecture of Vladimir Voevodsky regarding C-systems. This conjecture provides, under some assumptions, a lift of a functor $M\colon \mathrm{CC} \rightarrow \mathcal{C}$, where $\mathrm{CC}$ is a…
We define a notion of grading of a monoid T in a monoidal category C, relative to a class of morphisms M (which provide a notion of M-subobject). We show that, under reasonable conditions (including that M forms a factorization system),…
The category ${\rm Rel}(\mathcal{C})$ may be formed for any category $\mathcal{C}$ with finite limits using the same objects as $\mathcal{C}$ but whose morphisms from $X$ to $Y$ are binary relations in $\mathcal{C}$, that is, subobjects of…
Let $\mathcal C$ be a category with finite colimits, and let $(\mathcal E,\mathcal M)$ be a factorisation system on $\mathcal C$ with $\mathcal M$ stable under pushouts. Writing $\mathcal C;\mathcal M^{\mathrm{op}}$ for the symmetric…
Given an arbitrary countably generated rigid C*-tensor category, we construct a fully-faithful bi-involutive strong monoidal functor onto a subcategory of finitely generated projective bimodules over a simple, exact, separable, unital…
In this paper we consider the class of l-bijective C-systems, i.e., C-systems for which the length function is a bijection. The main result of the paper is a construction of an isomorphism between two categories - the category of…
Let $\mathcal C$ be a class of modules over a ring $R$, closed under direct sums over index sets of cardinality $\kappa$ and isomorphisms, and such that the isomorphism classes form a set. The monoid of modules $V(\mathcal C)$ encodes the…
For an endofunctor $F\colon\mathcal{C}\to\mathcal{C}$ on an ($\infty$-)category $\mathcal{C}$ we define the $\infty$-category $\operatorname{Cart}(\mathcal{C},F)$ of generalized Cartier modules as the lax equalizer of $F$ and the identity.…
In this study, we interpret the notion of homotopy of morphisms in the category of crossed modules in a category $\mathsf{C}$ of groups with operations using the categorical equivalence between crossed modules and internal categories in…
In the theory of operads we consider functors of generalized symmetric powers defined by sums of coinvariant modules under actions of symmetric groups. One observes classically that the construction of symmetric functors provides an…
We establish a relative monadicity theorem for relative monads with dense roots in a virtual equipment, specialising to a relative monadicity theorem for enriched relative monads. In particular, for a dense $\mathbb V$-functor $j \colon A…
We establish a duality between monads and monadic morphisms in any $(\infty,2)$-category and characterize monadic morphisms in a wide class of examples. This duality unifies several dualities between algebraic structures and their…