Cartesian Double Theories

A Double-Categorical Framework for Categorical Doctrines
Topos Institute Berkeley Seminar

Michael Lambert

University of Massachusetts-Boston

Evan Patterson

Topos Institute

2023-09-25

Categorical logic

Originates with the Functorial semantics of algebraic theories (Lawvere 1963):

Category Theory	Logic
small cartesian category $\mathsf{T}$	algebraic theory
cartesian functor $M: \mathsf{T} \to \mathsf{Set}$	model of theory
natural transformation $M \Rightarrow N$	model homomorphism

Categorical logic is inherently two-dimensional.

Landscape of categorical logic

Fragment of the “monoidal hierarchy” important in ACT:

Landscape of categorical logic

Fragment of the “standard hierarchy” of categorical logic:

Navigating the landscape

Implications of categorical logic:

Logic is part of mathematics, not the other way around
Foundations are pluralistic: choose, or build, a logic for the task at hand

But how to organize all of these logics?

Each logic is, at minimum, a 2-category
Arrows in the diagrams are forgetful 2-functors

Doctrines

What is a doctrine?

Doctrines are “categorified theories”
A theory specifies a set (or sets) equipped with extra structure
A doctrine specifies a category (or categories) with extra structure

OK, but what is a doctrine, really?

“Doctrine,” like “theory,” is not a precise term
“Doctrine” can be made precise in different ways
My interest: need organizing principle for computational category theory

Generalized algebraic theories

Any “purely algebraic” (higher) categorical structure is a model of a GAT.

GAT is short for generalized algebraic theory (Cartmell 1986)
GAT = “algebraic theory + dependent types”
Same expressivity as finite limit theories/essentially algebraic theories
Foundational role in Catlab.jl and now Gatlab.jl

GATs are great, but they are not doctrines.

GATs have 1-categories of models
Doctrine must give, at minimum, a 2-category of models

Doctrines as 2-monads

The standard answer: a doctrine is a 2-monad on $\mathbf{Cat}$.

There are 2-monads whose algebras are symmetric monoidal categories, categories with finite products, categories with finite limits, …
Have strict, pseudo, and lax morphisms of algebras
And have transformations of those, hence have 2-categories of algebras

A powerful theory, but hard to work with concretely:

No simple way to present 2-monads by generators and relations
Unclear how to do computer algebra with 2-monads

Doctrines as categorified algebraic theories

One-dimensional	Two-dimensional
Monad on $\mathsf{Set}$	2-monad on $\mathbf{Cat}$
Algebraic theory	???

Motivation:

Finitary monads $\simeq$ Lawvere theories (single-sorted algebraic theories)
Finite product theories (algebraic theories) are easily presentable by generators and relations

Questions:

What is a categorified finite product theory?
How to achieve two-dimensional functorial semantics?

Toward two-dimensional functorial semantics

Bénabou (1967) observed that a lax functor

\[ F: \mathsf{1} \to \mathbf{Span} \]

from the terminal category to the bicategory $\mathbf{Span}$ of

sets
spans
(feet-preserving) maps of spans

is the same thing as a small category.

Observation generalizes in interesting ways
So, are bicategories and lax functors enough for 2D functorial semantics?

Toward two-dimensional functorial semantics

No: the well-behaved cells

or icons between span-valued lax functors, correspond to identity-on-object functors between categories.

Toward two-dimensional functorial semantics

A lax functor

\[ F: \mathbb{1} \to \mathbb{S}\mathsf{pan} \]

from the terminal double category to the double category $\mathbb{S}\mathsf{pan}$ of

sets
functions
spans
maps of spans

is again the same thing as a small category.

Toward two-dimensional functorial semantics

But now natural transformations

between span-valued lax double functors correspond precisely to functors.

This simple observation is the beginning of a much bigger story…

Double theories

The big picture:

A “double theory” is a small double category $\mathbb{T}$ with extra structure
A model of a double theory is structure-preserving lax functor $\mathbb{T} \to \mathbb{S}\mathsf{pan}$
Models of a double theory are objects of a (possibly virtual) double category, even a (virtual) equipment

We develop this picture in detail, for two kinds of double theories:

Simple double theories, based on bare double categories
Cartesian double theories, based on double categories with finite products

Simple double theories: overview

Concept	Definition
Simple double theory	Small, strict double category $\mathbb{T}$
Model of simple double theory	Lax functor $F: \mathbb{T} \to \mathbb{S}\mathsf{pan}$
Morphism between models (strict, pseudo, op/lax)	(Strict, pseudo, op/lax) natural transformation $\alpha: F \Rightarrow G$
Bimodule between models	Module $M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G$
Cell between morphisms/bimodules	Modulation

Cartesian double theories: overview

Concept	Definition
Cartesian double theory	Small, cartesian, strict double category $\mathbb{T}$
Model of theory	Cartesian lax functor $F: \mathbb{T} \to \mathbb{S}\mathsf{pan}$
Model morphism (strict, pseudo, op/lax)	Cartesian (strict, pseudo, op/lax) natural transformation $\alpha: F \Rightarrow G$
Model bimodule	Cartesian module $M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G$
Cell	Modulation

Outline of talk

Lax double functors
Simple double theories and models
Cartesian double theories and models

Double categories: notation and terminology

A (pseudo) double category $\mathbb{D}$ is a pseudocategory in $\mathbf{Cat}$:

So, a double category $\mathbb{D}$ consists of

a category $\mathbb{D}_0$ of objects $x, y, \dots$ and arrows $f: x \to y$
a category $\mathbb{D}_1$ of proarrows $m, n, \dots$ and cells $\alpha: m \to n$

$\dots$

Double categories: notation and terminology

$\dots$

functors $s,t: \mathbb{D}_1 \rightrightarrows \mathbb{D}_0$, giving a source and target to proarrows $m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}y$ and cells
functors $\odot: \mathbb{D}_1 \times_{\mathbb{D}_0} \mathbb{D}_1 \to \mathbb{D}_1$ and $\operatorname{id}: \mathbb{D}_0 \to \mathbb{D}_1$, the external (horizontal) composition and identity

that are associative and unital up to coherent globular isomorphism.

Lax double functors

Lax functors between double categories preserve composition

strictly in the strict direction
laxly in the pseudo direction

Lax double functor

A lax functor $F: \mathbb{D} \to \mathbb{E}$ between double categories $\mathbb{D}$ and $\mathbb{E}$ consists of

functors $F_0: \mathbb{D}_0 \to \mathbb{E}_0$ and $F_1: \mathbb{D}_1 \to \mathbb{E}_1$ preserving source and target
for proarrows $x \overset{m}{\mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}} y \overset{n}{\mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}} z$ and objects $x$ in $\mathbb{D}$, laxator and unitor cells in $\mathbb{E}$

obeying axioms similar to (in fact, generalizing) a lax monoidal functor:

associativity and unitality of comparison cells
naturality of comparison cells

Naturality of laxators

Axiom:

for any two externally composable cells in $\mathbb{D}$:

Lax functors give categories

Proposition

Let $\mathbb{D}$ be a strict double category and let $F: \mathbb{D} \to \mathbb{S}\mathsf{pan}$ be a lax functor.

For object $x \in \mathbb{D}$, the data $(Fx, F\operatorname{id}_x, F_{x,x}, F_x)$ is a category, where
- set $Fx$ is objects
- span $F\operatorname{id}_x$ is morphisms with (co)domain maps
- laxator $F_{x,x}: F\operatorname{id}_x \odot F\operatorname{id}_x \to F\operatorname{id}_x$ is composition
- unitor $F_x: \operatorname{id}_{Fx} \to F\operatorname{id}_x$ is identities
For arrow $f: x \to y$ in $\mathbb{D}$, the data $(Ff, F\operatorname{id}_f)$ is a functor, where
- $Ff: Fx \to Fy$ is object map
- $F\operatorname{id}_f: F\operatorname{id}_x \to F\operatorname{id}_y$ is morphism map, preserving (co)domains
- Functorality is exactly naturality of laxators and unitors of $F$
For cell $\alpha: f \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}g$ in $\mathbb{D}$ with identity (co)domain, cell $F\alpha$ is a natural transformation
- proof is slightly more involved

Double functorial semantics

We can consider target double categories besides $\mathbb{S}\mathsf{pan}$.

Example: Spans

For any category $\mathsf{S}$ with pullbacks, there is a double category $\mathbb{S}\mathsf{pan}(\mathsf{S})$ with

objects, objects of $\mathsf{S}$;
arrows, morphisms of $\mathsf{S}$;
proarrows, spans in $\mathsf{S}$;
cells, maps of spans in $\mathsf{S}$.

External composition is by pullback in $\mathsf{S}$.

Proposition: Lax double functors $F: \mathbb{D} \to \mathbb{S}\mathsf{pan}(\mathsf{S})$ give categories, functors, and natural transformations internal to $\mathsf{S}$.

Double functorial semantics

Example: Matrices

For any (infinitary) distributive monoidal category $\mathcal{V}$, there is a double category $\mathcal{V}\text{-}\mathbb{M}\mathsf{at}$ with

objects, sets;
arrows, functions;
proarrows $M: X \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}Y$, functions $M: X \times Y \to \mathcal{V}$, called $\mathcal{V}$-matrices;
cells $\alpha: M \to N$ with source $f: X \to W$ and target $g: Y \to Z$, families of morphisms in $\mathcal{V}$ \[ \alpha_{x,y}: M(x,y) \to N(f(x), g(y)), \qquad x \in X,\ y \in Y.\]

External composition is by “matrix multiplication” with $\otimes$ as multiplication and coproduct as addition.

Proposition: Lax double functors $F: \mathbb{D} \to \mathcal{V}\text{-}\mathbb{M}\mathsf{at}$ give categories, functors, and natural transformations enriched in $\mathcal{V}$.

Lax functors give profunctors

Proposition

Let $\mathbb{D}$ be a strict double category and let $F: \mathbb{D} \to \mathbb{S}\mathsf{pan}$ be a lax functor.

For each proarrow $m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}y$ in $\mathbb{D}$, the data $(Fm, F_{x,m}, F_{m,y})$ is a profunctor, where
- span $Fm$ is heteromorphisms with source/target maps
- laxators $F_{x,m}$ and $F_{m,y}$ are left/right actions
For each cell $\alpha: m \to n$ in $\mathbb{D}$, the cell $F\alpha$ is a map of profunctors, i.e., a natural transformation

Moreover, replacing $\mathbb{S}\mathsf{pan}$ with…

$\mathbb{S}\mathsf{pan}(\mathsf{S})$ gives profunctors and profunctor maps internal to $\mathsf{S}$
$\mathcal{V}\text{-}\mathbb{M}\mathsf{at}$ gives profunctors and profunctor maps enriched in $\mathcal{V}$.

Summary: all concepts are lax double functors?

Concept of lax double functor contains all basic definitions of category theory:

categories
functors
natural transformations
profunctors
maps of profunctors

First strong evidence for a double-categorical framework for doctrines!

Simple double theories

The most basic notion of “double theory”
But already contains most of the key ideas
Plus a few interesting examples of doctrines, such as
- adjunctions
- monads

Simple double theories and models

Terminology:

A simple double theory is a small, strict double category $\mathbb{T}$
A model of a simple double theory $\mathbb{T}$ in a double category $\mathbb{S}$ is a lax functor $F: \mathbb{T} \to \mathbb{S}$
The double category $\mathbb{S}$ is called the semantics
By default, semantics is $\mathbb{S}\mathsf{pan}$ (or, equivalently, $\mathbb{M}\mathsf{at}$)

Analogy:

(Co)presheaves are ubiquitous in pure and applied category theory
Models of simple double theories are lax copresheaves

Example: theory of monads

The theory of monads $\mathbb{T}_{\mathsf{Mnd}}$ is generated by

an object $x$
an arrow $t: x \to x$
multiplication and unit cells

subjects to three equations expressing associativity and unitality.

Example: theory of monads

E.g., the associativity axiom:

\[=\]

A model of $\mathbb{T}_{\mathsf{Mnd}}$ is a category $\mathsf{C}$ along with a monad $(T,\mu,\eta)$ on $\mathsf{C}$
What about the model morphisms?

Lax transformations

A lax natural transformation $\alpha: F \Rightarrow G$ between lax double functors $F, G: \mathbb{D} \to \mathbb{E}$ consists of

for each object $x \in \mathbb{D}$, the component at $x$, an arrow in $\mathbb{E}$ \[ \alpha_x: Fx \to Gx \]
for each proarrow $m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}y$ in $\mathbb{D}$, the component at $m$, a cell in $\mathbb{E}$

$\dots$

Lax transformations

$\dots$

for each arrow $f: x \to y$, the naturality comparison at $f$, a cell in $\mathbb{E}$

subject to suitable naturality and functorality axioms (not stated).

Example: monad functors

A lax transformation between models $(\mathsf{C},S)$ and $(\mathsf{D},T)$ of $\mathbb{T}_{\mathsf{Mnd}}$ consists of

a functor $U: \mathsf{C} \to \mathsf{D}$
- given by the components at $x$ and $\operatorname{id}_x: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$
a natural transformation $\phi: T \circ U \Rightarrow U \circ S$
- given by the naturality comparison at $t: x \to x$

compatible with the monad multiplications and units.

This is precisely a monad functor as in Street’s formal theory of monads (1972).

Glimpse of the higher structure (I)

Theorem: 2-category of lax functors

For any double categories $\mathbb{D}$ and $\mathbb{E}$, there is a 2-category whose

objects are lax functors $F: \mathbb{D} \to \mathbb{E}$
morphisms are lax natural transformations $\alpha: F \Rightarrow G$
2-morphisms are modulations $\mu: \alpha \Rrightarrow\beta$.

So, every simple double theory has a 2-category of models
For example, the 2-category of models of $\mathbb{T}_{\mathsf{Mnd}}$ is equivalent to Street’s 2-category of monads (1972).

Glimpse of the higher structure (II)

Theorem: (virtual) double category of lax functors

For any double categories $\mathbb{D}$ and $\mathbb{E}$, there is a unital virtual double category $\mathbb{L}\mathsf{ax}_\ell(\mathbb{D},\mathbb{E})$ whose

objects are lax functors $F: \mathbb{D} \to \mathbb{E}$
arrows are lax natural transformations $\alpha: F \to G$
proarrows are modules $M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G$
multicells are multimodulations.

Moreover, when $\mathbb{D}$ is 2-categorical (has only trivial proarrows) and $\mathbb{E}$ has local coequalizers, there is a genuine double category $\mathbb{L}\mathsf{ax}_\ell(\mathbb{D},\mathbb{E})$.

So:

Every simple double theory $\mathbb{T}$ has a unital virtual double category of models
When $\mathbb{T}$ is 2-categorical, it has a double category of models

Cartesian double theories

Simple double theories are not very expressive
By adding finite products, far more doctrines can be expressed

Cartesian double categories

A double category $\mathbb{D}$ is cartesian if

underlying categories $\mathbb{D}_0$ and $\mathbb{D}_1$ have finite products, preserved by source and target $s, t: \mathbb{D}_1 \rightrightarrows \mathbb{D}_0$;
external composition $\odot: \mathbb{D}_1 \times_{\mathbb{D}_0} \mathbb{D}_1 \to \mathbb{D}_1$ and identity $\operatorname{id}: \mathbb{D}_0 \to \mathbb{D}_1$ also preserve finite products.

Example: Spans

When $\mathsf{S}$ is a category with finite limits, $\mathbb{S}\mathsf{pan}(\mathsf{S})$ is a cartesian double category.

Example: Matrices

When $\mathcal{V}$ is an (infinitary) distributive category, $\mathcal{V}\text{-}\mathbb{M}\mathsf{at}$ is a cartesian double category.

Cartesian lax functors and transformations

A lax double functor $F: \mathbb{D} \to \mathbb{E}$ is cartesian if the underlying functors $F_0: \mathbb{D}_0 \to \mathbb{E}_0$ and $F_1: \mathbb{D}_1 \to \mathbb{E}_1$ preserve finite products

A lax natural transformation $\alpha: F \Rightarrow G: \mathbb{D} \to \mathbb{E}$ is cartesian if it strictly natural with respect to projections, meaning that
- for all pairs $x, x' \in \mathbb{D}$, the naturality squares commute
- and the naturality comparisons $\alpha_{\pi_{x,x'}}$ and $\alpha_{\pi_{x,x'}'}$ are given by unitors of $G$.

Cartesian double theories and models

Terminology:

A cartesian double theory is a small, cartesian, strict double category $\mathbb{T}$
A model of a cartesian double theory $\mathbb{T}$ in a cartesian double category $\mathbb{S}$ is a cartesian lax functor $F: \mathbb{T} \to \mathbb{S}$
A (strict, pseudo, or lax) morphism of models is a cartesian (strict, pseudo, or lax) natural transformation between models

Analogy:

Finite product theories/algebraic theories are small cartesian categories
Cartesian double theories categorify those

Models of cartesian double theories: examples

(co)presheaves
monoidal categories (strict and weak)
braided and symmetric monoidal categories
monoidal (co)presheaves
multicategories
cartesian and cocartesian categories
rig categories and distributive monoidal categories
…

Example: theory of pseudomonoids

The theory of pseudomonoids $\mathbb{T}_{\mathsf{PsMon}}$ is generated by

an object $x$
arrows $\otimes: x^2 \to x$ and $I: 1 \to x$
associator and unitor cells, along with their external inverses,

subject to two equations, the pentagon and triangle identities.

A model of $\mathbb{T}_{\mathsf{PsMon}}$ is a (weak) monoidal category.

Example: theory of promonoids

The theory of promonoids $\mathbb{T}_{\mathsf{Promon}}$ is generated by

an object $x$
proarrows $p: x^2 \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$ and $j: 1 \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$

subject to the axioms of

associativity: $(p \times \operatorname{id}_x) \odot p = (\operatorname{id}_x \times p) \odot p: x^3 \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$
unitality: $(j \times \operatorname{id}_x) \odot p = \operatorname{id}_x = (\operatorname{id}_x \times j) \odot p: 1 \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$.

Example: theory of promonoids

A model of $\mathbb{T}_{\mathsf{Promonoid}}$ is a multicategory:

object $x$ is sent to set of objects
for each arity $n$, unique proarrow $p_n: x^n \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-10mu{\to}}x$ is sent to multispan of $n$-ary multimorphisms
laxators and unitors give composition operations and identities

Illustrates an interesting ~~bug~~ feature of lax functors:

Giving a model of a finitely presented double theory may require giving an infinite amount of data
Classical logic is not like this!

Summary

Cartesian double theories are a framework for categorical doctrines based on double functorial semantics
Includes most of the “monoidal hierarchy” of doctrines, plus much else
Seems to exclude most of the “standard hierarchy” of doctrines, starting with categories with finite limits

Present and future work

The forthcoming paper includes much not covered here:

Many more double theories, plus proofs of their correctness
Careful constructions of the (virtual) double categories of models of simple and cartesian double theories
When semantics is a cartesian equipment, (virtual) equipments of models and pseudo morphisms of models
Restriction sketches: double theories with equipment-like structure
Another perspective on models: equivalence between lax span-valued functors and normal lax profunctor-valued functors

As for future work… there is a lot!

References

Aleiferi, Evangelia. 2018. “Cartesian Double Categories with an Emphasis on Characterizing Spans.” PhD thesis, Dalhousie University. https://arxiv.org/abs/1809.06940.

Bénabou, Jean. 1967. “Introduction to Bicategories.” In Reports of the Midwest Category Seminar, 1–77. https://doi.org/10.1007/BFb0074299.

Blackwell, R., G. M. Kelly, and A. J. Power. 1989. “Two-Dimensional Monad Theory.” Journal of Pure and Applied Algebra 59 (1): 1–41. https://doi.org/10.1016/0022-4049(89)90160-6.

Cartmell, John. 1986. “Generalised Algebraic Theories and Contextual Categories.” Annals of Pure and Applied Logic 32: 209–43. https://doi.org/10.1016/0168-0072(86)90053-9.

Cruttwell, G. S. H., and Michael A. Shulman. 2010. “A Unified Framework for Generalized Multicategories.” Theory and Applications of Categories 24 (21): 580–655. http://www.tac.mta.ca/tac/volumes/24/21/24-21abs.html.

Grandis, Marco. 2019. Higher Dimensional Categories: From Double to Multiple Categories. World Scientific. https://doi.org/10.1142/11406.

Grandis, Marco, and Robert Paré. 1999. “Limits in Double Categories.” Cahiers de Topologie Et géométrie Différentielle Catégoriques 40 (3): 162–220.

Lack, Stephen. 2010. “A 2-Categories Companion.” In Towards Higher Categories, edited by John C. Baez and J. Peter May, 105–91. Springer. https://doi.org/10.1007/978-1-4419-1524-5_4.

Lawvere, F. William. 1963. “Functorial Semantics of Algebraic Theories.” PhD thesis, Columbia University. http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html.

———. 1969. “Ordinal Sums and Equational Doctrines.” In Seminar on Triples and Categorical Homology Theory, 141–55. https://doi.org/10.1007/BFb0083085.

Paré, Robert. 2011. “Yoneda Theory for Double Categories.” Theory and Applications of Categories 25 (17): 436–89. http://www.tac.mta.ca/tac/volumes/25/17/25-17abs.html.

———. 2013. “Composition of Modules for Lax Functors.” Theory and Applications of Categories 27 (16): 393–444. http://www.tac.mta.ca/tac/volumes/27/16/27-16abs.html.

Shulman, Michael. 2008. “Framed Bicategories and Monoidal Fibrations.” Theory and Applications of Categories 20 (18): 650–738. http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html.

Street, Ross. 1972. “The Formal Theory of Monads.” Journal of Pure and Applied Algebra 2 (2): 149–68. https://doi.org/10.1016/0022-4049(72)90019-9.

Wood, Richard J. 1982. “Abstract Proarrows I.” Cahiers de Topologie Et géométrie Différentielle 23 (3): 279–90.

Category Theory	Logic
small cartesian category \(\mathsf{T}\)	algebraic theory
cartesian functor \(M: \mathsf{T} \to \mathsf{Set}\)	model of theory
natural transformation \(M \Rightarrow N\)	model homomorphism

One-dimensional	Two-dimensional
Monad on \(\mathsf{Set}\)	2-monad on \(\mathbf{Cat}\)
Algebraic theory	???

Concept	Definition
Simple double theory	Small, strict double category \(\mathbb{T}\)
Model of simple double theory	Lax functor \(F: \mathbb{T} \to \mathbb{S}\mathsf{pan}\)
Morphism between models (strict, pseudo, op/lax)	(Strict, pseudo, op/lax) natural transformation \(\alpha: F \Rightarrow G\)
Bimodule between models	Module \(M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\)
Cell between morphisms/bimodules	Modulation