An adjunction $𝐹⊣𝑈$ with $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒟︀}$ and $𝑈:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$ induces a monad $𝑇=𝑈\circ 𝐹$ on $\mathrm{𝒞︀}$. Write $𝜀:𝐹\circ 𝑈\Rightarrow \text{𝖨𝖽}$ for the counit of the adjunction. Every object $𝑑$ of $\mathrm{𝒟︀}$ then induces a $𝑇$-algebra carried by the object $𝑈𝑑$, witnessed by the map

This assignment extends to a functor into the Eilenberg–Moore category,

the comparison functor of the adjunction.

Dually, an adjunction induces a comonad on the other side and a comparison into the co-Eilenberg–Moore category. When these comparisons are equivalences we say that the adjunction $𝐹⊣𝑈$ is (co)monadic.

A well-founded order is a set $𝐷$ with a proposition-valued transitive relation $<$ admitting no infinite descent: every element is accessible. Write $𝑎\le 𝑏$ for $(𝑎<𝑏)\vee (𝑎=𝑏)$.

A direct structure on a category $\mathrm{𝒞︀}$ over $(𝐷,<)$ is a functor

into the well-founded order viewed as a poset category. The functor organizes two pieces of data at once: an ordering on the objects, and the invariant that morphisms respect it — $𝑓:𝑥\to 𝑦$ forces $\text{deg}𝑥\le \text{deg}𝑦$.

A direct structure equips the objects with a well-founded strict relation

Intuitively, direct categories are the right generalization of well-foundedness to the categorical setting: a direct category is essentially one whose underlying graph is a directed acyclic graph, layered by degree, so that data at an object may be defined by recursion from data at all objects strictly below it.

The degrees order the objects, while the morphisms of $\mathrm{𝒞︀}$ say how an object sits over its predecessors.

Later takes a limit over smaller indices. Dually, the earlier modality takes a colimit over larger indices: an element of $⊲𝑃$ at $𝑥$ is a $𝑃$-element sitting at some object $𝑦$ strictly above $𝑥$, carried down along a chosen morphism $𝑥\to 𝑦$.

Earlier is left adjoint to later:

Under this adjunction, $\text{𝗇𝖾𝗑𝗍}:𝑃\to ⊳𝑃$ corresponds to

.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. An initial $𝐹$-algebra, written $𝜇𝐹$, is an initial object of the category of algebras $\text{Alg}(𝐹)$.

Unfolding the universal property: an initial algebra is an algebra $(𝜇𝐹,\text{in})$ such that every algebra $(𝑥,𝛼)$ admits a unique morphism $\text{fold}𝛼:𝜇𝐹\to 𝑥$ satisfying

Conjugation with the adjunction between presheaves and families $𝑈⊣\text{Cofree}$ lets us induce a later construction on families from the one on presheaves,

Concretely, later on families evaluates to

The later modality for presheaves on a direct category is given by the presheaf of natural transformations

out of the strict downset.

An element of $⊳𝑃$ at $𝑥$ is a coherent choice of $𝑃$-elements at all objects strictly smaller than $𝑥$.

Restriction in $⊳𝑃$ along $𝑓:𝑦\to 𝑥$ precomposes with the induced map $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑦)\to \text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)$. At an object of minimal degree the strict downset is empty, so $⊳𝑃$ is trivial there.

Via functoriality, every presheaf restricts to smaller indices. Thus we may define the map

that sends an element $𝑝$ over $𝑥$ to the family of all its restrictions along morphisms from strictly lower objects.

Like later on families, the recursion principle for families is inherited from that on presheaves. Given a family $𝐴$ and a step

the construction is a chain of transpositions with Löb for presheaves used in the middle:

Just as for presheaves, the fixed point constructed above is unique: the two transpositions are bijections, and the presheaf-level fixed point is already unique.

Let $\mathrm{𝒞︀}$ be a direct category and $𝑃$ a presheaf on it. Every map

has a fixed point: a global element $\text{𝗅ö𝖻}𝜑:\top \to 𝑃$ with

and this fixed point is unique.

The hypothesis says: the value of $𝑃$ at any object is determined by its values over the strict past — $𝜑$ turns a coherent family over the strict downset of $𝑥$ into a value at $𝑥$. The proof is recursion along the well-founded $\prec$: at each $𝑥$, the section already constructed over the past assembles into an element of $(⊳𝑃)(𝑥)$, and $𝜑$ extends it to $𝑥$.

Write $𝑋\Rightarrow 𝑌$ for the presheaf of morphisms $𝑋\to 𝑌$. An endofunctor $𝐹$ on presheaves is locally contractive when its action on morphisms factors through later: there is a map

An adjunction $𝐹⊣𝑈$ with $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒟︀}$ and $𝑈:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$ induces a monad $𝑇=𝑈\circ 𝐹$ on $\mathrm{𝒞︀}$, and a comparison functor

sending each object of $\mathrm{𝒟︀}$ to the $𝑇$-algebra it carries.

The functor $𝑈$ is monadic when $𝐾$ is an equivalence: the adjunction exhibits $\mathrm{𝒟︀}$ as objects of $\mathrm{𝒞︀}$ equipped with algebraic structure for $𝑇$, the Eilenberg–Moore category.

Comonadicity is monadicity in the opposite category: a left adjoint $𝐿:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$ with right adjoint $𝑅$ induces a comonad $𝑊=𝐿\circ 𝑅$ on $\mathrm{𝒞︀}$, a comparison $\mathrm{𝒟︀}\to \text{coEM}(𝑊)$ into the co-Eilenberg–Moore category, and $𝐿$ is comonadic when this comparison is an equivalence.

The adjoint triple $\text{Free}⊣𝑈⊣\text{Cofree}$ induces a monad $𝑇=𝑈\circ \text{Free}$ and a comonad $𝑊=𝑈\circ \text{Cofree}$ on $\text{Fam}(\mathrm{𝒞︀})$.

Both comparison functors are equivalences: presheaves are the Eilenberg–Moore algebras of $𝑇$ and the co-Eilenberg–Moore coalgebras of $𝑊$,

So presheaves are both monadic and comonadic over families.

Reading the algebra structure concretely: a $𝑇$-algebra on a family $𝐴$ is a map ${\sum }_{𝑦}\mathrm{𝒞︀}(𝑥,𝑦)\times 𝐴(𝑦)\to 𝐴(𝑥)$ for each $𝑥$, subject to the monad algebra laws — that is, exactly a functorial action of restriction.

The comonadic reading is the same structure seen from the element’s side: a $𝑊$-coalgebra is a map $𝐴(𝑥)\to {\prod }_{𝑦}\mathrm{𝒞︀}(𝑦,𝑥)\to 𝐴(𝑦)$, giving each value its restriction along every morphism into $𝑥$. Where the monad says restriction acts on values, the comonad says a value already carries all of its restrictions — and the coalgebra laws say it does so coherently.

The representable $\text{𝗒}𝑥$ is itself a sieve on $𝑥$. A sieve on $𝑥$ is proper when it is not equal to the representable.

Say that a proper sieve is maximal when it contains all other proper sieves as a sub-sieve.

A sieve on an object $𝑥$ of $\mathrm{𝒞︀}$ is a subobject of the representable presheaf $\text{𝗒}𝑥$: a presheaf $𝑆$ with a monic morphism $𝑆\rightarrowtail \text{𝗒}𝑥$. Sieves are a generalization from the notion of ideal found in ring theory to category theory.

A morphism $𝑓:𝑦\to 𝑥$ belongs to $𝑆$, written $𝑆\ni 𝑓$, when $𝑓$ lies in the image of the inclusion at $𝑦$. Because $𝑆$ is a presheaf and the inclusion is natural, membership is closed under precomposition:

A sieve is thus a “downward closed” collection of morphisms into $𝑥$.

Sieves on $𝑥$ are ordered by refinement: $𝑆\subseteq 𝑇$ when every morphism belonging to $𝑆$ belongs to $𝑇$.

Call a direct structure reflecting when every morphism between objects of equal degree is a split epimorphism. In a reflecting direct category, every non-invertible-in-degree morphism strictly raises degree, and the strict downset is as large as a proper sieve can be:

If the direct structure is reflecting, then every proper sieve $𝑆$ on $𝑥$ refines into the strict downset:

Suppose $𝑓\in 𝑆$ with $𝑓:𝑦\to 𝑥$ of equal degree. By reflection $𝑓$ has a section $𝑠$, and closure under precomposition gives $𝑠\star 𝑓={\text{𝗂𝖽}}_{𝑥}\in 𝑆$, contradicting properness.

So every morphism in $𝑆$ strictly raises degree. That is, every morphism in $𝑆$ is also a member of $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)$.

Let $\mathrm{𝒞︀}$ carry a direct structure. The strict downset $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)$ of an object $𝑥$ is the presheaf of morphisms into $𝑥$ from strictly lower objects:

with restriction by precomposition — well defined since degrees are non-decreasing, so precomposing can only stay strictly below.

The evident inclusion $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)\rightarrowtail よ𝑥$ makes $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)$ a sieve on $𝑥$. It is moreover a proper sieve, as it exlcudes the identity.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. A terminal $𝐹$-coalgebra, written $𝜈𝐹$, is a terminal object of the category of coalgebras $\text{Coalg}(𝐹)$ — equivalently, an initial algebra for ${𝐹}^{\text{op}}$.

Unfolding the universal property: a terminal coalgebra is a coalgebra $(𝜈𝐹,\text{out})$ such that every coalgebra $(𝑥,𝛾)$ admits a unique morphism $\text{unfold}𝛾:𝑥\to 𝜈𝐹$ satisfying

A category $\mathrm{𝒞︀}$ consists of

1. A type of objects ${\mathrm{𝒞︀}}_0$
2. For each pair of objects $𝑥,𝑦:{\mathrm{𝒞︀}}_0$ a set of morphisms $\mathrm{𝒞︀}(𝑥,𝑦)$. We may simply write a morphism with an arrow, denote $𝑓:\mathrm{𝒞︀}(𝑥,𝑦)$ as $𝑓:𝑥\to 𝑦$ or $𝑥\stackrel{𝑓}{\to }𝑦$ or similar
3. A composition operation on morphisms. For $𝑓:𝑥\to 𝑦$ and $𝑔:𝑦\to 𝑧$, there is a morphism $𝑓\star 𝑔:𝑥\to 𝑧$
4. For each $𝑥:{\mathrm{𝒞︀}}_0$, an identity morphism ${\text{𝗂𝖽}}_{𝑥}:𝑥\to 𝑥$

5. Left-unitality of composition: for all $𝑓:𝑥\to 𝑦$, an equality

   $${\text{𝗂𝖽𝖫}}_{𝑓}:{\text{𝗂𝖽}}_{𝑥}\star 𝑓=𝑓$$

6. Right-unitality of composition: for all $𝑓:𝑥\to 𝑦$, an equality

   $${\text{𝗂𝖽𝖱}}_{𝑓}:𝑓\star {\text{𝗂𝖽}}_{𝑦}=𝑓$$

7. Associativity of composition: for all $𝑓:𝑥\to 𝑦$, $𝑔:𝑦\to 𝑧$, $ℎ:𝑧\to 𝑤$, an equality

   $${\text{𝖺𝗌𝗌𝗈𝖼}}_{𝑓,𝑔,ℎ}:(𝑓\star 𝑔)\star ℎ=𝑓\star (𝑔\star ℎ)$$

Concretely, the definition above is meant to model the one used in the Cubical standard library [1].

However, the notion of category is flexible. Depending on the context, we may be talking of small, locally small, wild, or any other kind of category that may augment which things we require to be (homotopy) sets, which things we require to be small types, etc. For the most part, the same idea of a category will apply across all of these settings.

A bicategory is a notion of weak 2-category that arises as a category weakly enriched in categories. That is, instead of having hom sets, between any two objects a bicategory has hom categories such that the enriched category laws hold up to invertible 2-cell rather than strictly.

A bicategory $\mathrm{𝒦︀}$ consists of

1. A type of objects ${\mathrm{𝒦︀}}_0$, or 0-cells
2. For all $𝑥,𝑦:{\mathrm{𝒦︀}}_0$, a category ${\mathrm{𝒦︀}}_1(𝑥,𝑦)$. We may elide the subscript and simply write this as $\mathrm{𝒦︀}(𝑥,𝑦)$. Refer to the objects of $\mathrm{𝒦︀}(𝑥,𝑦)$ as 1-cells between $𝑥$ and $𝑦$, and we may write $𝑓:\mathrm{𝒦︀}(𝑥,𝑦)$ as $𝑓:𝑥\to 𝑦$ or $𝑥\stackrel{𝑓}{\to }𝑦$. For $𝑓,𝑔:\mathrm{𝒦︀}(𝑥,𝑦)$, refer to the morphisms in $\mathrm{𝒦︀}(𝑥,𝑦)$ between $𝑓$ and $𝑔$ as 2-cells and write the morphism $𝛼:(\mathrm{𝒦︀}(𝑥,𝑦))(𝑓,𝑔)$ as $𝛼:𝑓\Rightarrow 𝑔$ or $𝑓\stackrel{𝛼}{\Rightarrow }𝑔$
3. For each $𝑥:{\mathrm{𝒦︀}}_0$, an identity 1-cell $1_{𝑥}:\mathrm{𝒦︀}(𝑥,𝑥)$
4. For all $𝑥,𝑦,𝑧:{\mathrm{𝒦︀}}_0$, a composition functor ${\mathrm{𝒦︀}}_{\star }^{𝑥,𝑦,𝑧}:\mathrm{𝒦︀}(𝑥,𝑦)\times \mathrm{𝒦︀}(𝑦,𝑧)\to \mathrm{𝒦︀}(𝑥,𝑧)$. For 1-cells $𝑓:𝑥\to 𝑦$ and $𝑔:𝑦\to 𝑧$, write their composite as $𝑓\star 𝑔:𝑥\to 𝑧$

5. For all $𝑤,𝑥,𝑦,𝑧:{\mathrm{𝒦︀}}_0$, a natural isomorphism, the associator $𝛼$ between the two composite functors $\mathrm{𝒦︀}(𝑤,𝑥)\times \mathrm{𝒦︀}(𝑥,𝑦)\times \mathrm{𝒦︀}(𝑦,𝑧)\to \mathrm{𝒦︀}(𝑤,𝑧)$ that compose the leftmost, respectively rightmost, pair first:

   $${\mathrm{𝒦︀}}_{\star }^{𝑤,𝑦,𝑧}\circ ({\mathrm{𝒦︀}}_{\star }^{𝑤,𝑥,𝑦}\times \text{id})\Rightarrow {\mathrm{𝒦︀}}_{\star }^{𝑤,𝑥,𝑧}\circ (\text{id}\times {\mathrm{𝒦︀}}_{\star }^{𝑥,𝑦,𝑧})$$

   Its component at 1-cells $𝑓,𝑔,ℎ$ is the invertible 2-cell

   $${𝛼}_{𝑓,𝑔,ℎ}:(𝑓\star 𝑔)\star ℎ\Rightarrow 𝑓\star (𝑔\star ℎ)$$

6. For all $𝑥,𝑦:{\mathrm{𝒦︀}}_0$, natural isomorphisms, the left unitor $𝜆$ and right unitor $𝜌$, each between an endofunctor of $\mathrm{𝒦︀}(𝑥,𝑦)$ and the identity functor:

   $${\mathrm{𝒦︀}}_{\star }^{𝑥,𝑥,𝑦}\circ ⟨1_{𝑥},\text{id}⟩\Rightarrow \text{id}{\mathrm{𝒦︀}}_{\star }^{𝑥,𝑦,𝑦}\circ ⟨\text{id},1_{𝑦}⟩\Rightarrow \text{id}$$

   where $1_{𝑥}$ and $1_{𝑦}$ in the pairings $⟨-,-⟩$ denote the constant functors at the identity 1-cells. The components at a 1-cell $𝑓:\mathrm{𝒦︀}(𝑥,𝑦)$ are the invertible 2-cells

   $${𝜆}_{𝑓}:1_{𝑥}\star 𝑓\Rightarrow 𝑓{𝜌}_{𝑓}:𝑓\star 1_{𝑦}\Rightarrow 𝑓$$

7. such that for all $𝑓:\mathrm{𝒦︀}(𝑥,𝑦)$ and $𝑔:\mathrm{𝒦︀}(𝑦,𝑧)$ the triangle below commutes in $\mathrm{𝒦︀}(𝑥,𝑧)$:

8. and such that for all composable 1-cells $𝑓,𝑔,ℎ,𝑘$ the pentagon below commutes:

Fix a bicategory $\mathrm{𝒦︀}$, with composition $\star$, identity 1-cells $1_{𝑥}$, associator $𝛼$, and unitors $𝜆,𝜌$. A monad in $\mathrm{𝒦︀}$ internalises the usual notion of monad: it is an endo-1-cell carrying a multiplication and a unit that satisfy the monoid laws up to the coherence cells of the bicategory.

A monad in $\mathrm{𝒦︀}$ consists of

1. a 0-cell $𝑥$, the object the monad acts on;
2. an endo-1-cell $𝑡:\mathrm{𝒦︀}(𝑥,𝑥)$;
3. a multiplication 2-cell $𝜇:𝑡\star 𝑡\Rightarrow 𝑡$;
4. a unit 2-cell $𝜂:1_{𝑥}\Rightarrow 𝑡$;

5. such that $𝜇$ is associative: the following diagram of 2-cells commutes in $\mathrm{𝒦︀}(𝑥,𝑥)$, where the top map is the associator that rebrackets the threefold composite:

6. and such that $𝜇$ and $𝜂$ satisfy the unit laws: the following two diagrams commute in $\mathrm{𝒦︀}(𝑥,𝑥)$, where the hypotenuses are the left and right unitors:

Taking $\mathrm{𝒦︀}$ to be the bicategory of categories, functors, and natural transformations recovers an ordinary monad on a category: $𝑡$ is the endofunctor, $𝜇$ the multiplication, and $𝜂$ the unit, with the coherence cells all identities.

Fix a set $𝑋$. The objects of the free monoidal category over $𝑋$, $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$, are generated inductively by the elements of $𝑋$ and a unit element $𝐼$ over a binary operation $\otimes$. The morphisms are given by a quotient-inductive type. They are generated by associators, unitors, and identity over composition and parallel action over $\otimes$ then quotiented by associativity and composition equation to satisfy the category laws, equations constraining the associators/unitors to be natural isomorphisms, and pentagon/triangle equations to satiate the axioms of a monoidal category.

Given any displayed monoidal category ${𝑀}^{\text{𝙳}}$ over $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$ with an interpretation $𝜄:𝑋⇝{𝑀}^{\text{𝙳}}$, we may construct a global section $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)\to {𝑀}^{\text{𝙳}}$. We refer to this as the global elimination principle of $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$.

A quiver is just a directed graph presented via a type of objects, a type of edges, and two projection functions that pick out source and target of an edge.

A category $𝐶$ is thin if there is at most one morphism between any two objects.

An element of a presheaf $𝑃$ at an object $𝑐$ is an element $𝑥$ of the set $𝑃𝑐$.

A universal element of a presheaf $𝑃$ on a category $𝐶$ is an element $𝑥\in 𝑃𝑐$, where $𝑐$ is some object of $𝐶$, demonstrating that $𝑃$ is representable by $𝑐$.

(Slightly) more concretely, a universal element is captured by the following three pieces of data

• An object $𝑐$ of $𝐶$
• An element $𝑥\in 𝑃𝑐$
• A proof that the map sending a morphism $𝑓:𝑏\to 𝑐$ to $(𝑃𝑓)(𝑥)$ is an equivalence

This third point states that morphisms from $𝑏$ into $𝑐$ are uniquely determined by an element of $𝑃$ at the domain $𝑏$.

Or equivalently, universal elements are terminal in the category of elements.

The constant presheaf of a set $𝑋$ on a category $𝐶$ is a functor $\mathrm{\Delta }(𝑋):{𝐶}^{𝑜𝑝}\to \text{𝐒𝐞𝐭}$ such that

I often call this the discrete presheaf for $𝑋$, but I don’t know if that’s standard.

In a category $\mathrm{𝒞︀}$, a subobject of $𝑐$ is an isomorphism class of monomorphisms into $𝑐$.

An object $𝑐$ in a category $\mathrm{𝒞︀}$ is terminal if there is a unique morphism from any other object into it.

Because terminal objects are unique up to unique isomorphism (as are all universal objects) we often just write $\top$ to refer to the terminal object. Likewise, $!:𝑑\to \top$ refers to the unique morphism into $\top$.

Let $𝑐$ and $𝑑$ be objects in a category $\mathrm{𝒞︀}$ with two parallel morphisms $𝑓,𝑔:𝑐\to 𝑑$. The equalizer of $𝑓$ and $𝑔$, if it exists, is the universal object $\text{𝖾𝗊}$ with the following property:

• There is a morphism $𝜋:\text{𝖾𝗊}\to 𝑐$
• $𝑓\circ 𝜋=𝑔\circ 𝜋$

Subsets $𝐴$ of a set $𝑋$ may classically be identified with a characteristic map ${𝜒}_{𝐴}:𝑋\to \text{𝖻𝗈𝗈𝗅}$. Intuitively, for every $𝑥:𝑋$, ${𝜒}_{𝐴}$ gives a truth value to the statement “$𝑥$ is in the subset $𝐴$”. In this manner, the domain of the characteristic map, $\text{𝖻𝗈𝗈𝗅}$, classifies the subsets of $𝑋$.

Generalizing over this principle, in a category $\mathrm{𝒞︀}$ an object $\mathrm{\Omega }$ is a subobject classifier if maps into it from some object $𝑐$ likewise uniquely identify a subobject of $𝑐$.

We can understand $\mathrm{\Omega }$ to behave like an object of truth values that are not necessarily boolean valued. A morphism $𝑝:𝑐\to \mathrm{\Omega }$ can be thought of like a predicate on $𝑐$. If $𝑐$ were a set, this would precisely be the characteristic function on it. However, this idea can generalize beyond sets. For instance in the category of graphs, $\mathrm{\Omega }$ is a cleverly constructed graph such that any graph homomorphism $𝑔\to \mathrm{\Omega }$ into it picks out a unique subgraph of $𝑔$.

There are always two (suggestively named) disjoint “points” of $\mathrm{\Omega }$, thought of as morphisms out of the terminal object $\text{𝗍𝗋𝗎𝖾},\text{𝖿𝖺𝗅𝗌𝖾}:\top \to \mathrm{\Omega }$. I think if we’re being careful, $\text{𝗍𝗋𝗎𝖾}$ may properly be the “subobject classifier” but I always use the term to refer to $\mathrm{\Omega }$ itself.

A subobject $𝜙:𝑑\hookrightarrow 𝑐$ induces a unique characteristic morphism ${𝑝}_{𝜙}:𝑐\to \mathrm{\Omega }$ such that

Moreover, the appropriate square must be a pullback.

A monoidal category is left closed if for each $𝑌\in 𝐶$, the functor $-\otimes 𝑌:𝐶\to 𝐶$ has a right adjoint $𝑌⊸-:𝐶\to 𝐶$ forming the left internal-hom out of $𝑌$.

That is, for all $𝑋,𝑌,𝑍$, there is a natural isomorphism $𝐶[𝑋\otimes 𝑌,𝑍]\cong 𝐶[𝑋,[𝑌,𝑍]]$

There is an obvious right-handed variant $𝑌⟜-$ that is right adjoint to $𝑌\otimes -$.

If $𝐶$ is both right and left closed, the monoidal category is simply called closed (or perhaps biclosed).

The bicategory of categories $\text{𝖢𝖠𝖳}$ has

• as 0-cells, categories (at a fixed pair of universe levels, for objects and for morphisms);
• as hom-category $\text{𝖢𝖠𝖳}(\mathrm{𝒞︀},\mathrm{𝒟︀})$, the functor category $[\mathrm{𝒞︀},\mathrm{𝒟︀}]$, so 1-cells are functors and 2-cells are natural transformations;
• as identity 1-cell, the identity functor;

• as composition, $𝐹\star 𝐺=𝐺\circ 𝐹$ on functors. On natural transformations $𝛽:𝐹\Rightarrow 𝐹\prime$ and $𝛾:𝐺\Rightarrow 𝐺\prime$ the horizontal composite is given directly by its components

  $${(𝛽\star 𝛾)}_{𝑐}=𝐺({𝛽}_{𝑐})\star {𝛾}_{𝐹\prime 𝑐}.$$

Every component of the left unitor, the right unitor and the associator is an identity morphism, and their inverses are identities too. So the only content of the triangle and pentagon is that composites of identities are identities.

$\text{𝖢𝖠𝖳}$ is still a bicategory and not a strict 2-category: $\text{Id}\circ 𝐹$ and $𝐹$ agree on objects and on morphisms, but in the formalization they are not the same functor definitionally. The structure cells are there to name that agreement.

A monad in $\text{𝖢𝖠𝖳}$ is an ordinary monad on a category, and a prestack is a pseudofunctor into $\text{𝖢𝖠𝖳}$.

Let $𝑃$ be a presheaf on a category $\mathrm{𝒞︀}$. The category of elements of $𝑃$ is the displayed category over $\mathrm{𝒞︀}$ whose displayed objects over $𝑐$ are the elements $𝑝\in 𝑃𝑐$, and whose displayed morphisms over $𝑓:𝑐\to 𝑑$ from $𝑝$ to $𝑞$ are proofs that $(𝑃𝑓)(𝑞)=𝑝$.

Since $𝑃𝑐$ is a set, there is at most one displayed morphism over each $𝑓$ between given elements: a morphism of elements is a morphism of $\mathrm{𝒞︀}$ that happens to carry $𝑞$ back to $𝑝$. Its total category is the classical category of elements $\int 𝑃$, and a universal element of $𝑃$ is exactly a terminal object of $\int 𝑃$.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. An algebra $𝛼:𝐹𝐵\to 𝐵$ is corecursive when for every coalgebra $𝛾:𝑋\to 𝐹𝑋$ there is exactly one hylomorphism from $𝛾$ to $𝛼$. Equivalently, the functor $\text{𝖧𝗒𝗅𝗈}(-,𝛼)$ of the hylomorphism profunctor is constantly a singleton. It is the dual of a recursive coalgebra: an $𝐹$-algebra in $\mathrm{𝒞︀}$ is corecursive exactly when it is recursive as an ${𝐹}^{\text{op}}$-coalgebra in ${\mathrm{𝒞︀}}^{\text{op}}$.

Example. If $(𝜈𝐹,\text{𝗈𝗎𝗍})$ is a terminal coalgebra, then $\text{𝗈𝗎𝗍}$ is invertible and ${\text{𝗈𝗎𝗍}}^{-1}:𝐹(𝜈𝐹)\to 𝜈𝐹$ is a corecursive algebra: a solution of $ℎ=𝛾\star 𝐹ℎ\star {\text{𝗈𝗎𝗍}}^{-1}$ is the same thing as a solution of $ℎ\star \text{𝗈𝗎𝗍}=𝛾\star 𝐹ℎ$, that is, a coalgebra map into the terminal coalgebra, and there is exactly one, $\text{𝗎𝗇𝖿𝗈𝗅𝖽}𝛾$.

Let $\mathrm{𝒱︀}$ be a symmetric monoidal closed category that is complete and cocomplete. Let $\left(\mathrm{𝒞︀},{\otimes }_{\mathrm{𝒞︀}},𝐼\right)$ be a small monoidal $\mathrm{𝒱︀}$-enriched category and $𝐴,𝐵$ be $\mathrm{𝒱︀}$-enriched presheaves on $\mathrm{𝒞︀}$. Define

Then, for Day convolution ${\otimes }_{\text{Day}}$,

Symmetrically, $(𝐵⟜𝐴)𝑐={\int }_{𝑣}𝐴𝑣{⊸}_{\mathrm{𝒱︀}}𝐵\left(𝑐{\otimes }_{\mathrm{𝒞︀}}𝑣\right)$ and $-{\otimes }_{\text{Day}}𝐴⊣-⟜𝐴$, so the enriched presheaf category $[{\mathrm{𝒞︀}}^{\text{op}},\mathrm{𝒱︀}]$ is biclosed [1].

Let $\mathrm{𝒱︀}$ be a symmetric monoidal closed category that is complete and cocomplete. Let $\left(\mathrm{𝒞︀},{\otimes }_{\mathrm{𝒞︀}},𝐼\right)$ be a small monoidal $\mathrm{𝒱︀}$-enriched category. The Day convolution of $\mathrm{𝒱︀}$-enriched presheaves $𝐴,𝐵:{\mathrm{𝒞︀}}^{\text{op}}\to \mathrm{𝒱︀}$ is the enriched presheaf

with unit the representable $\mathrm{𝒞︀}(-,𝐼)$.

Day convolution makes the enriched presheaf category $[{\mathrm{𝒞︀}}^{\text{op}},\mathrm{𝒱︀}]$ a monoidal category, symmetric when $\mathrm{𝒞︀}$ is [1]. It is moreover closed.

Under the enriched Yoneda embedding the convolution of representables is representable, $\mathrm{𝒞︀}(-,𝑥){\otimes }_{\text{Day}}\mathrm{𝒞︀}(-,𝑦)\cong \mathrm{𝒞︀}\left(-,𝑥{\otimes }_{\mathrm{𝒞︀}}𝑦\right)$, so Day convolution is the cocontinuous extension of the tensor of $\mathrm{𝒞︀}$.

Let $𝐶$ be a small monoidal category. Recall that for presheaves $𝐴,𝐵:{𝐶}^{\text{op}}\to \text{𝐒𝐞𝐭}$, the Day convolution provides a closed monoidal structure:

which forms an adjunction $𝐴\otimes -⊣𝐴⊸-$.

For covariant functors $𝐴:𝐶\to \text{𝐒𝐞𝐭}$ and presheaves $𝐵:{𝐶}^{\text{op}}\to \text{𝐒𝐞𝐭}$, we can define the quotient and its right adjoint, each of which is a presheaf on $𝐶$:

These form the adjunction ${𝐷}_{𝐴}⊣\sqrt[𝐴]{-}$.

The Day quotient, ${𝐷}_{𝐴}𝐵$, takes $𝐴$ to be a covariant functor and $𝐵$ to be a contravariant one. While the residual $𝐴⊸𝐵$ takes both to be contravariant.

This apparent variance mismatch disappears when we restrict to the groupoid core $𝐺=\text{𝖼𝗈𝗋𝖾}(𝐶)$, where variance is trivialized since $𝐺\cong {𝐺}^{\text{op}}$.

For any functor $𝐹:𝐺\to \text{𝐒𝐞𝐭}$ on the core, we can freely extend it to both a presheaf and a covariant copresheaf on $𝐶$ by left Kan extension along the respective inclusions $𝐺\to {𝐶}^{\text{op}}$ and $𝐺\to 𝐶$:

By substituting these extensions into the definitions of the residual and the quotient, we obtain a general coincidence for any $𝐹:𝐺\to \text{𝐒𝐞𝐭}$ and $𝐵:{𝐶}^{\text{op}}\to \text{𝐒𝐞𝐭}$:

This equivalence states that computing the residual against the presheaf extension of $𝐹$ is perfectly isomorphic to taking the quotient by its covariant extension.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$, a coalgebra $𝛾:𝑋\to 𝐹𝑋$ and an algebra $𝛼:𝐹𝐵\to 𝐵$. A hylomorphism (or coalgebra-to-algebra morphism) from $𝛾$ to $𝛼$ is a morphism $ℎ:𝑋\to 𝐵$ satisfying

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. Hylomorphisms form a profunctor from coalgebras to algebras,

where $\text{𝖧𝗒𝗅𝗈}((𝑋,𝛾),(𝐵,𝛼))$ is the set of $ℎ:𝑋\to 𝐵$ with $ℎ=𝛾\star 𝐹ℎ\star 𝛼$.

The action is by composition. If $𝑔:(𝑌,𝛿)\to (𝑋,𝛾)$ is a coalgebra morphism ($𝑔\star 𝛾=𝛿\star 𝐹𝑔$) and $𝑘:(𝐵,𝛼)\to (𝐵\prime ,𝛼\prime )$ is an algebra morphism ($𝛼\star 𝑘=𝐹𝑘\star 𝛼\prime$), then $𝑔\star ℎ\star 𝑘$ is again a hylomorphism:

In these terms, a coalgebra $𝛾$ is recursive when $\text{𝖧𝗒𝗅𝗈}(𝛾,-)$ is the terminal functor, and an algebra $𝛼$ is corecursive when $\text{𝖧𝗒𝗅𝗈}(-,𝛼)$ is. For the inverse of an initial algebra the profunctor is representable, $\text{𝖧𝗒𝗅𝗈}({\text{𝗂𝗇}}^{-1},-)\cong \text{𝖠𝗅𝗀}(𝐹)(\text{𝗂𝗇},-)$, and dually $\text{𝖧𝗒𝗅𝗈}(-,{\text{𝗈𝗎𝗍}}^{-1})\cong \text{𝖢𝗈𝖺𝗅𝗀}(𝐹)(-,\text{𝗈𝗎𝗍})$ for a terminal coalgebra.

When every value of $\text{𝖧𝗒𝗅𝗈}$ is a singleton, every divide-and-conquer specification over $𝐹$ has exactly one solution. This is what local contractivity guarantees.

A lax functor $𝐹:\mathrm{ℬ︀}\to \mathrm{𝒞︀}$ between bicategories consists of

1. a map on 0-cells, $𝑥\mapsto 𝐹𝑥$;
2. for all $𝑥,𝑦$, a functor ${𝐹}_{𝑥,𝑦}:\mathrm{ℬ︀}(𝑥,𝑦)\to \mathrm{𝒞︀}(𝐹𝑥,𝐹𝑦)$, acting on 1-cells and 2-cells;
3. a unit comparison, natural 2-cells ${𝐹}_{𝑥}^0:1_{𝐹𝑥}\Rightarrow 𝐹(1_{𝑥})$;
4. a composition comparison, 2-cells ${𝐹}_{𝑓,𝑔}^2:𝐹𝑓\star 𝐹𝑔\Rightarrow 𝐹(𝑓\star 𝑔)$ natural in $𝑓$ and $𝑔$;

5. such that three coherence laws hold, one for each structure cell of $\mathrm{ℬ︀}$:

   • left unit: $({𝐹}^0▷𝐹𝑓)\star {𝐹}_{1,𝑓}^2\star 𝐹({𝜆}_{𝑓})={𝜆}_{𝐹𝑓}$;
   • right unit: $(𝐹𝑓◁{𝐹}^0)\star {𝐹}_{𝑓,1}^2\star 𝐹({𝜌}_{𝑓})={𝜌}_{𝐹𝑓}$;
   • associativity: $({𝐹}_{𝑓,𝑔}^2▷𝐹ℎ)\star {𝐹}_{𝑓\star 𝑔,ℎ}^2\star 𝐹({𝛼}_{𝑓,𝑔,ℎ})={𝛼}_{𝐹𝑓,𝐹𝑔,𝐹ℎ}\star (𝐹𝑓◁{𝐹}_{𝑔,ℎ}^2)\star {𝐹}_{𝑓,𝑔\star ℎ}^2$.