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 a countably infinite set of names $𝔸$. A nominal set [1] is a set $𝑋$ equipped with an action by the group of finite permutations $\text{𝖯𝖾𝗋𝗆}(𝔸)$, such that every element $𝑥\in 𝑋$ has a finite support.

A finite set of names $𝑆\subseteq 𝔸$ supports $𝑥$ if any permutation fixing $𝑆$ pointwise also fixes $𝑥$.

The category of nominal sets is equivalent to the Schanuel topos. Under this equivalence, a nominal set $𝑋$ corresponds to a functor $𝕀\to \text{𝐒𝐞𝐭}$, where $𝕀$ is the category of finite sets and injections, given by mapping a finite set of names $𝑡$ to the set of elements supported by $𝑡$:

In the Schanuel topos, the underlying category for Day convolution is $𝐶={𝕀}^{\text{op}}$, where $𝕀$ is the category of finite sets and injections.

Given a nominal set $𝑋$, its presheaf action describes elements supported by $𝑡$:

Instead of taking $𝑋$ a priori as a presheaf, we can view it as a finitely- supported $\text{𝖯𝖾𝗋𝗆}(𝔸)$-set. We can restrict our attention to the groupoid core $𝐺=\text{𝖼𝗈𝗋𝖾}(𝕀)$, asking for the support to be exactly the input:

This family ${𝑋}_{•}:𝐺\to \text{𝐒𝐞𝐭}$ is functorial on finite sets and bijections.

By extending this functor along the inclusions described in Quotient Coincidence, we can extend ${𝑋}_{•}$ to both a presheaf $\text{𝗆𝗄𝖯𝗌𝗁}({𝑋}_{•})$ and a copresheaf $\text{𝗆𝗄𝖢𝗈𝗉𝗌𝗁}({𝑋}_{•})$ on $𝐶$. This suggests the equivalence:

I suspect this allows us to describe name abstraction $[𝑋]𝑌$ [1] —which ordinarily looks like an operation on two presheaves of the same variance—as the quotient of $𝑌$ by the induced copresheaf $\text{𝗆𝗄𝖢𝗈𝗉𝗌𝗁}({𝑋}_{•})$.

Concretely, $[𝑋]𝑌$ is usually given by the quotient of the product by an equivalence relation:

where $(𝑥,𝑦)\sim (𝜋𝑥,𝜋𝑦)$ for permutations $𝜋$ fixing $\text{𝗌𝗎𝗉𝗉}(𝑦)-\text{𝗌𝗎𝗉𝗉}(𝑥)$.

On the other hand, the Day quotient computes to a coend:

A priori, a coend over $𝑠$ of the product ${𝑋}_{𝑠}\times 𝑌(𝑠\uplus 𝑐)$ is expressed as the quotient of a set of triples by an equivalence relation $\approx$:

However, because the comprehension formula fixes $𝑠=\text{𝗌𝗎𝗉𝗉}(𝑥)$, we reduce to a quotient of pairs:

I suspect that this quotient will equate to the one given by $[𝑋]𝑌$, thus resolving the apparent issues with variance. I further suspect that one will need the sheaf condition (pullback-preservation) of nominal sets to establish this equivalence.

Let $𝕀$ be the category of finite sets and injections. The Schanuel topos is the category of pullback-preserving functors ${𝕀}^{\text{op}}\to \text{𝐒𝐞𝐭}$.

Equivalently, it is the category of nominal sets, which are sets equipped with an action by the group of permutations on a countable set of names $𝔸$, such that every element has finite support.

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].

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{𝖢𝖠𝖳}$.

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{𝗎𝗇𝖿𝗈𝗅𝖽}𝛾$.

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$.

Here $\star$ between 2-cells is vertical composition, and $𝜃▷ℎ$ and $ℎ◁𝜃$ are whiskerings.

Lax functors compose: ${(𝐺\circ 𝐹)}^0={𝐺}^0\star 𝐺({𝐹}^0)$ and ${(𝐺\circ 𝐹)}_{𝑓,𝑔}^2={𝐺}_{𝐹𝑓,𝐹𝑔}^2\star 𝐺({𝐹}_{𝑓,𝑔}^2)$. The coherence laws of the composite follow from those of $𝐹$ and $𝐺$ and naturality of ${𝐺}^2$, without using the triangle or pentagon of any of the bicategories involved.

A lax functor whose comparison cells are invertible is a pseudofunctor.

Let $𝐹,𝐺:\mathrm{ℬ︀}\to \mathrm{𝒞︀}$ be lax functors. A lax natural transformation $𝜎:𝐹\Rightarrow 𝐺$ consists of

1. for each 0-cell $𝑥$, a 1-cell ${𝜎}_{𝑥}:𝐹𝑥\to 𝐺𝑥$;

2. for each 1-cell $𝑓:𝑥\to 𝑦$, a 2-cell filling the naturality square,

   $${𝜎}_{𝑓}:𝐹𝑓\star {𝜎}_{𝑦}\Rightarrow {𝜎}_{𝑥}\star 𝐺𝑓;$$
3. such that ${𝜎}_{𝑓}$ is natural in $𝑓$: for a 2-cell $𝜃:𝑓\Rightarrow 𝑔$, $(𝐹𝜃▷{𝜎}_{𝑦})\star {𝜎}_{𝑔}={𝜎}_{𝑓}\star ({𝜎}_{𝑥}◁𝐺𝜃)$;
4. and such that $𝜎$ respects the comparison cells of $𝐹$ and $𝐺$: one law relating ${𝜎}_{1_{𝑥}}$ to ${𝐹}^0$, ${𝐺}^0$ and the unitors, and one relating ${𝜎}_{𝑓\star 𝑔}$ to ${𝜎}_{𝑓}$, ${𝜎}_{𝑔}$, ${𝐹}^2$, ${𝐺}^2$ and the associators.

A lax natural transformation is pseudonatural when every ${𝜎}_{𝑓}$ is invertible. As with pseudofunctors, this is a property, so the pseudonatural transformations $𝐹\Rightarrow 𝐺$ are a full subcategory of the category of lax transformations and modifications.

Between prestacks the 1-cells are taken to be pseudonatural. The reason is biuniversality: a transformation whose components ${𝜎}_{𝑥}$ are all equivalences of categories is an equivalence of prestacks only if its naturality cells are invertible, and a biuniversal element should be exactly a representation of a prestack up to such an equivalence.

Every category $\mathrm{𝒞︀}$ is a bicategory $\text{𝖫𝖣}(\mathrm{𝒞︀})$ with only identity 2-cells. Its 0-cells are the objects of $\mathrm{𝒞︀}$, and the hom-category $\text{𝖫𝖣}(\mathrm{𝒞︀})(𝑥,𝑦)$ is the discrete category on the set $\mathrm{𝒞︀}(𝑥,𝑦)$: a 2-cell $𝑓\Rightarrow 𝑔$ is a proof that $𝑓=𝑔$. Composition and identities are those of $\mathrm{𝒞︀}$; the unitors and associator are the unit and associativity laws of $\mathrm{𝒞︀}$. Since the homs of $\mathrm{𝒞︀}$ are sets, any two parallel 2-cells are equal, so the triangle and pentagon hold trivially.

A functor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒟︀}$ gives a pseudofunctor $\text{𝖫𝖣}(𝐹):\text{𝖫𝖣}(\mathrm{𝒞︀})\to \text{𝖫𝖣}(\mathrm{𝒟︀})$, whose comparison 2-cells are the functor laws of $𝐹$.

The locally discrete bicategory is how ordinary indexed categories enter bicategorical language: a prestack on $\text{𝖫𝖣}(\mathrm{𝒞︀})$ is a pseudofunctor ${\mathrm{𝒞︀}}^{\text{op}}\to \text{𝖢𝖠𝖳}$, and its Grothendieck construction is a displayed category over $\mathrm{𝒞︀}$.

The opposite ${\mathrm{ℬ︀}}^{\text{op}}$ of a bicategory $\mathrm{ℬ︀}$ has the same 0-cells and reverses the 1-cells but not the 2-cells:

Composition swaps its arguments, $𝑓{\star }^{\text{op}}𝑔=𝑔\star 𝑓$. The left unitor of ${\mathrm{ℬ︀}}^{\text{op}}$ is the right unitor of $\mathrm{ℬ︀}$ and vice versa, and the associator of ${\mathrm{ℬ︀}}^{\text{op}}$ is the inverse of the associator of $\mathrm{ℬ︀}$, with its arguments reversed.

Since the 2-cells keep their direction, a lax functor $𝐹:\mathrm{ℬ︀}\to \mathrm{𝒞︀}$ induces a lax (not oplax) functor ${\mathrm{ℬ︀}}^{\text{op}}\to {\mathrm{𝒞︀}}^{\text{op}}$ with the same action on cells. Reversing the 2-cells instead gives the bicategory ${\mathrm{ℬ︀}}^{\text{co}}$, whose hom-categories are the opposites ${(\mathrm{ℬ︀}(𝑥,𝑦))}^{\text{op}}$.

Duality saves work: a coherence lemma about $\mathrm{ℬ︀}$ can often be obtained by instantiating a companion lemma at ${\mathrm{ℬ︀}}^{\text{op}}$, which swaps left and right.

A pseudofunctor $𝐹:\mathrm{ℬ︀}\to \mathrm{𝒞︀}$ is a lax functor whose unit and composition comparisons

are invertible 2-cells. So $𝐹$ preserves identities and composition up to coherent isomorphism.

Being pseudo is a property of a lax functor: invertibility of a 2-cell is a proposition, since inverses are unique. The data of a pseudofunctor is exactly the data of a lax functor, and everything proved about lax functors applies to pseudofunctors unchanged. Pseudofunctors are closed under composition and identities, as lax functors are, because invertible 2-cells are closed under composition and under the action of a functor on hom-categories.

The main examples here are prestacks, pseudofunctors ${\mathrm{ℬ︀}}^{\text{op}}\to \text{𝖢𝖠𝖳}$. When $\mathrm{ℬ︀}$ is locally discrete on a category $\mathrm{𝒞︀}$, these are the pseudofunctors ${\mathrm{𝒞︀}}^{\text{op}}\to \text{𝖢𝖠𝖳}$ of fibred category theory.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. A coalgebra $𝛾:𝑋\to 𝐹𝑋$ is recursive when for every algebra $𝛼:𝐹𝐵\to 𝐵$ there is exactly one hylomorphism $ℎ:𝑋\to 𝐵$ from $𝛾$ to $𝛼$, that is, exactly one solution of

Equivalently, the functor $\text{𝖧𝗒𝗅𝗈}(𝛾,-)$ of the hylomorphism profunctor is constantly a singleton.

Recursiveness is a coalgebraic form of well-foundedness: $𝛾$ decomposes each input into subproblems, and recursiveness says that every divide-and-conquer program built on this decomposition has a unique meaning, without mentioning an order on inputs. [1] use recursive coalgebras on categories of indexed families to obtain algorithms that are correct by the type of the map they compute.

Example. If $(𝜇𝐹,\text{𝗂𝗇})$ is an initial algebra, then $\text{𝗂𝗇}$ is invertible (Lambek’s lemma) and ${\text{𝗂𝗇}}^{-1}:𝜇𝐹\to 𝐹(𝜇𝐹)$ is a recursive coalgebra. Precomposing with the isomorphism $\text{𝗂𝗇}$, the equation $ℎ={\text{𝗂𝗇}}^{-1}\star 𝐹ℎ\star 𝛼$ is equivalent to $\text{𝗂𝗇}\star ℎ=𝐹ℎ\star 𝛼$, which says $ℎ$ is an algebra map out of the initial algebra; there is exactly one, $\text{𝖿𝗈𝗅𝖽}𝛼$.

The dual notion is a corecursive algebra.

The total bicategory of a displayed bicategory over $\mathrm{𝒦︀}$ packages the base and the displayed data together, one dimension up from the total category of a displayed category.

• Its 0-cells are pairs of a 0-cell of $\mathrm{𝒦︀}$ and a displayed 0-cell over it.
• Its hom-category from to is the total category of the displayed hom-category . So a 1-cell is a pair and a 2-cell is a pair .
• Identities, composition, unitors and associator are pairs of the base structure and the displayed structure over it, and the triangle and pentagon hold because they hold in the base and, over that, in the displayed bicategory.

Projecting to first components is a pseudofunctor whose unit and composition comparisons are identity 2-cells.

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: