For any string $𝑤$, we can define a representable grammar $\lceil 𝑤\rceil$ which matches exactly the string $𝑤$ and nothing else. The parse trees for a representable grammar are proofs that the string is exactly equal to $𝑤$:

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

The total category of a displayed category over $\mathrm{𝒞︀}$ collects the displayed data into a single category. Its objects are pairs of an object $𝑥$ of $\mathrm{𝒞︀}$ with an object over it, and its morphisms are pairs of a morphism $𝑓:𝑥\to 𝑦$ with a displayed morphism over $𝑓$.

Projecting out the first components is a functor . Constructions presented displayed — algebras, Eilenberg–Moore categories — get their forgetful functor for free as this projection.

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 displayed category over a base category $\mathrm{𝒞︀}$ packages the data of a category that “lies over” $\mathrm{𝒞︀}$: each object and each morphism of $\mathrm{𝒞︀}$ is equipped with a fiber of objects and morphisms displayed atop it. It consists of

1. For each object $𝑥:{\mathrm{𝒞︀}}_0$, a type of displayed objects lying over $𝑥$. We write for a displayed object over $𝑥$.
2. For each morphism $𝑓:\mathrm{𝒞︀}(𝑥,𝑦)$ and displayed objects and , a set of displayed morphisms lying over $𝑓$. We write such a displayed morphism as or , subscripting the arrow with the base morphism $𝑓$ it lies over.
3. A displayed composition operation. For $𝑓:𝑥\to 𝑦$ and $𝑔:𝑦\to 𝑧$ with displayed morphisms and , there is a displayed morphism lying over the composite $𝑓\star 𝑔$.
4. For each , a displayed identity lying over ${\text{𝗂𝖽}}_{𝑥}$.

5. Left-unitality, displayed: for all , a heterogeneous equality

6. Right-unitality, displayed: for all , a heterogeneous equality

7. Associativity, displayed: for all , , over $𝑓:𝑥\to 𝑦$, $𝑔:𝑦\to 𝑧$, $ℎ:𝑧\to 𝑤$, a heterogeneous equality

Because the type of displayed morphisms depends on the base morphism $𝑓$, the two sides of each displayed law inhabit different displayed hom-sets — those indexed by the two sides of the corresponding base-category equation. Each displayed law is therefore a heterogeneous equality $𝑎{=}_{𝑝}𝑏$: a path from $𝑎$ to $𝑏$ lying over the base path $𝑝$, rather than an equation within a single fixed set.

Concretely, this definition models the one used in the Cubical standard library [1].

A displayed category is to a category as a dependent type is to a context. In this way, displayed categories are effectively dependent categories, as we present the structure of as a category parametrized by the structure of $\mathrm{𝒞︀}$.

Displayed categories were introduced by Ahrens and Lumsdaine [2]. The point is that a displayed category over $\mathrm{𝒞︀}$ is equivalent to the data of a category $\mathrm{𝒟︀}$ together with a functor $𝐹:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$, but presented as families indexed by the objects and morphisms of $\mathrm{𝒞︀}$ — so that constructions like Grothendieck fibrations can be defined without ever invoking equality of objects.

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.

Given a displayed category over a category $\mathrm{𝒞︀}$ and another displayed category over , the total category of , we can define , the displayed total category of , as a displayed category over $\mathrm{𝒞︀}$.

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.

Given a displayed category over a category $\mathrm{𝒞︀}$ and a functor $𝐹:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$, the reindexing of along $𝐹$ is a displayed category over $\mathrm{𝒟︀}$. It is simply the portion of over the image of $𝐹$.

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

For categories $\mathrm{𝒞︀}$ and $\mathrm{𝒟︀}$, we can define the weakening of $\mathrm{𝒟︀}$ over $\mathrm{𝒞︀}$ as a displayed category over $\mathrm{𝒞︀}$ which trivially displays a copy of $\mathrm{𝒟︀}$ over each object of $\mathrm{𝒞︀}$.

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.

Let $𝐾$ be a ring and $𝐾[{𝑥}_0,\dots ,{𝑥}_{𝑛}]$ a polynomial ring over it. Suppose $𝐼\subset 𝐾[{𝑥}_0,\dots ,{𝑥}_{𝑛}]$ is an ideal. A Gröbner basis for $𝐼$ is a generating set of polynomials for the ideal that is minimal with respect to a given ordering on the monomials ${𝑥}_0,\dots ,{𝑥}_{𝑛}$.

Given an ideal $𝐼$, a Gröbner basis for $𝐼$ may be found via Buchberger’s algorithm. Intuitively, Buchberger’s algorithm attempts to solve a system of polynomial equations by iterated polynomial division to eliminate variables. At any given point, there is a degree of freedom in which what variable will be eliminated by the next division. The algorithm attempts to eliminate variables with respect to the monomial ordering.

Buchberger’s algorithm may be viewed simultaneously as a generalization of the Quine-McCluskey Boolean minimization algorithm and as a special case of the Knuth-Bendix algorithm.

The complexity of Buchberger’s algorithm is a little unwieldy to estimate in general. However, just like SAT solvers there are enough optimizations to execute Buchberger reasonably fast in practice. For instance, it is fast enough to handle several hundreds of polynomials, each having hundreds of terms with very large coefficients.

There are some very fun applications of this approach, such as Solving Sudoku with Algebra. This idea has also been applied to inferring polynomial loop invariants.

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.

Define a grammar for each finite cardinal $𝑛:\mathbb{N}$.

Then define the grammar of all finite cardinals as

Define a grammar $𝐴$ to be finitely unambiguous if $𝐴\&𝐴\cong 𝐴$.

There is likely a better name for this.