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 $𝑤$:

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.

A grammar $𝐴$ is unambiguous if the unique map into the terminal object is a monomorphism. That is, $𝐴$ is a subobject of $\top$.

A grammar $𝐴$ is unambiguous if for all grammars $𝐵$ and maps $𝑒,𝑒\prime :𝐴⊢𝐵$ we have $𝑒=𝑒\prime$.

In a category with terminal objects, this is equivalent to unambiguity defined via subterminality.

Finite unambiguity does not serve as an adequate definition of unambiguity that is equivalent to unambiguity as subterminality and unambiguity as a unique map. However, the definition attempted via finite unambiguity can be refined to something that is equivalent to these.

A grammar $𝐴$ is unambiguous if $\mathrm{\Delta }:𝐴⊢𝐴\&𝐴$ is an isomorphism. Equivalently, $𝐴$ is unambiguous if ${𝜋}_1:𝐴\&𝐴⊢𝐴$ and ${𝜋}_2:𝐴\&𝐴⊢𝐴$ are equal.

For a grammar $𝐴$, the Kleene star ${𝐴}^{\ast }$ is defined as a least-fixed point,

For a grammar $𝐴$, the Kleene star ${𝐴}^{\ast }$ is isomorphic to an indexed coproduct.

That is, we may view the parses of ${𝐴}^{\ast }$ like a linear list comprising parses of $𝐴$ concatenated together. Further, for each of these lists we may know the precise length.

When viewing Dependent Lambek Calculus as a model of Kleene algebra, this is precisely the statement that star continuity holds.

The first set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

The followlast set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

The nullability ($\text{𝖭𝗎𝗅𝗅}(\cdot )$) of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with one of the grammars

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 tensor of grammars,

is simply typed, so $𝐵$ cannot see what $𝐴$ matched.

Just as we have the generalization from the pair type $𝐴\times 𝐵$ to the dependent pair ${\mathrm{\Sigma }}_{𝑎:𝐴}𝐵𝑎$, we can define a dependent tensor operation. It is a $\mathrm{\Sigma }$-like generalization over the ordinary tensor, in which the second grammar depends on a parse tree of the first.

Write $\text{𝖳𝗋𝖾𝖾}(𝐴)={\sum }_{𝑤}𝐴(𝑤)$ for the type of parse trees of $𝐴$, each paired with the string it parses.

For a grammar $𝐴$ and a family of grammars $𝐵:\text{𝖳𝗋𝖾𝖾}(𝐴)\to \text{𝐆𝐫}$, the dependent tensor is:

We may also write it as $(𝑎\in 𝐴)\otimes 𝐵(𝑎)$.

When $𝐵$ is a constant family, the dependent tensor reduces to the ordinary tensor $𝐴\otimes 𝐵$.

Dependence runs left to right here, which fits left-to-right parsing. The other handedness, in which the first grammar depends on a parse of the second, is also definable.

For an alphabet $\mathrm{\Sigma }$, let ${\mathrm{\Sigma }}^{\ast }$ be the free monoid of strings over $\mathrm{\Sigma }$. A formal grammar $𝐴$ is a family of types indexed by strings:

This definition views formal grammars directly as indexed families of types over strings (which equivalently form presheaves on the discrete category of strings). This view forms the central notion of the Dependent Lambek Calculus. For a given string $𝑤$, the type $𝐴(𝑤)$ represents the type of all valid parse trees for $𝑤$ according to the grammar $𝐴$. If the grammar cannot parse $𝑤$, then $𝐴(𝑤)$ is the empty type.

When a grammar quotient ${𝐷}_{𝐴}𝐵$ is taken with respect to a representable grammar $𝐴=\lceil 𝑤\rceil$ (matching exactly the string $𝑤$), it coincides with the residual $𝐴⊸𝐵$, as established by the Quotient and Residual Coincidence.

This special case is known as the Brzozowski derivative of $𝐵$ by the string $𝑤$, often written as ${𝜕}_{𝑤}𝐵$. We have the following coincidence:

Write $𝑢⊏𝑣$ when $𝑢$ is a proper suffix of $𝑣$, that is, $𝑣=𝑥\text{++}𝑢$ with $𝑥\ne 𝜀$. The later of a grammar $𝐴$ is

A parse of $▷𝐴$ over $𝑣$ is a parse of $𝐴$ over every proper suffix of $𝑣$. In particular $(▷𝐴)𝜀$ is a singleton.

This is later on families for strings under the proper-suffix order. That order is well-founded because it strictly decreases length, so it is a thin direct category. There is at most one map $𝑢\to 𝑣$, so the product over maps from the strict past has one factor per proper suffix. Guarded recursion is modelled by presheaves on $𝜔$, the topos of trees, and more generally by sheaves over a well-founded base [1]. Here the later acts on families, which is what grammars are, and there is no clock.

Later is the right adjoint of the proper-suffix derivative. Let $\text{𝖭𝖤𝖲}={⨁}_{𝑥\ne 𝜀}\lceil 𝑥\rceil$ be the grammar of non-empty strings. Then the derivative $({𝜕}_{\text{𝖭𝖤𝖲}}𝐵)𝑢\cong {\sum }_{𝑥\ne 𝜀}𝐵(𝑥\text{++}𝑢)$ has the right adjoint

so ${𝜕}_{\text{𝖭𝖤𝖲}}-⊣▷$. Splitting $\text{𝖭𝖤𝖲}$ into its summands gives the form of $▷$ that the calculus can define:

The component at $𝑤$ says: if the string begins with $𝑤$, then the rest parses as $𝐴$.

The restriction to non-empty $𝑤$ is what makes this a later. At $𝑤=𝜀$ the component is $\sqrt[\lceil 𝜀\rceil ]{𝐴}\cong 𝐴$. Including it would give a projection $▷𝐴⊢𝐴$, and Löb would then prove every grammar. For the same reason the later is a product over suffixes. A sum such as ${⨁}_{𝑐}\lceil 𝑐\rceil ⊸𝐴$ is empty at $𝜀$, and at $𝐴=\perp$ it is $\perp$. The identity step $\perp ⊢\perp$ would then give Löb a proof of $\top ⊢\perp$.

In the Agda this is ▷ in Grammar/Later/Base.agda, which is defined as the indexed conjunction of √l-string. The mirror image ▷r, over proper prefixes, is defined in the same way. See also the bilateral later and the later along an arbitrary well-founded order.

For every grammar $𝐴$ and every term $𝜑:▷𝐴⊢𝐴$, where $▷$ is the later on grammars, there is a unique global parse $\text{𝗅ö𝖻}𝜑:\top ⊢𝐴$ with

Here $\text{𝗇𝖾𝗑𝗍}𝑡:\top ⊢▷𝐴$ restricts a global parse $𝑡$ to every proper suffix.

The proof is recursion on the length of the string. At $𝑣$, the parses already built at the proper suffixes of $𝑣$ form an element of $(▷𝐴)𝑣$, and $𝜑$ turns it into a parse at $𝑣$. Uniqueness is Löb for families over the proper-suffix order. In the Agda, lob in Grammar/Later/Base.agda is this recursion, done by well-founded induction on length.

To prove an entailment $𝐵⊢𝐶$ this way, apply Löb to $𝐴=𝐵\Rightarrow 𝐶$. The hypothesis $▷(𝐵\Rightarrow 𝐶)$ is the induction hypothesis at every proper suffix. It becomes usable once a non-nullable grammar has been consumed. If $𝜀\&𝐵⊢\perp$, then

because a parse of $𝐵\otimes \top$ over $𝑣$ splits $𝑣=𝑥\text{++}𝑢$ with $𝑥$ non-empty, so $𝑢⊏𝑣$. This is ▷-app-NE in Grammar/Later/Properties.agda. Induction on a Kleene star is the standard use.

For presheaves, $\text{𝗇𝖾𝗑𝗍}:𝑃\to ▷𝑃$ restricts along the strict past, as in later on presheaves. A grammar is only a family over strings, so a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ into the later on grammars is extra data. It sends a parse over $𝑣$ to parses over every proper suffix of $𝑣$.

Let $\square 𝐴=𝐴\&▷𝐴$, so that $(\square 𝐴)𝑣\cong {\prod }_{𝑢⊑𝑣}𝐴𝑢$. This is the comonad $𝑈\circ \text{Cofree}$ for the suffix order, and presheaves are comonadic over families. The counit law forces the first component of a coalgebra $𝐴⊢\square 𝐴$ to be the identity. Hence:

• a presheaf on strings under the suffix order is the same as a grammar $𝐴$ with a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ that satisfies coassociativity. Restricting to $𝑢\prime$ and then to $𝑢⊏𝑢\prime$ must agree with restricting to $𝑢$ directly;
• for a proposition-valued grammar (a language), coassociativity is automatic, and $\text{𝗇𝖾𝗑𝗍}$ exists exactly when the language is closed under suffixes. For example, $\top$ has one, but $\lceil 𝑎\rceil$ does not, since $(▷\lceil 𝑎\rceil )𝑎\cong \lceil 𝑎\rceil 𝜀$ is empty.

Löb does not need $\text{𝗇𝖾𝗑𝗍}$ on $𝐴$. The fixed-point equation only restricts a global parse $\top ⊢𝐴$, and a global parse can always be restricted. In the Agda, the grammar-level IsCoalgebra record, with only the field next, is in Grammar/Later/Coalgebra.agda on the guarded branch.

On presheaves the strict downset of $𝑐\text{++}𝑡$ is represented by $𝑡$, because every proper suffix of $𝑐\text{++}𝑡$ is a suffix of $𝑡$. So predecessors simplify later to $(▷𝑃)(𝑐\text{++}𝑡)\cong 𝑃𝑡$. On grammars there is no such simplification, since the factors at different suffixes are unrelated.

For formal grammars $𝐴$ and $𝐵$, the quotient of $𝐵$ by $𝐴$ is the grammar of what is left of $𝐵$ once an $𝐴$ has been read off the front:

A parse of the quotient consists of an $𝐴$-parses at prefix $𝑢$ and a $𝐵$-parse of the full string $𝑢·𝑣$.

This operation has a right adjoint:

Intuitively, $\sqrt[𝐴]{𝐶}$ parses $𝑤$ if: for all splittings of $𝑤$ into a prefix and suffix, if the prefix matches $𝐴$ then the suffix must match $𝐶$.

Together, these form the adjunction:

This is an instance of the Day quotient over the discrete monoidal category of strings.

For formal grammars $𝐴$ and $𝐵$, the residual $𝐴⊸𝐵$ (sometimes called the lollipop or linear implication) is the right adjoint to the grammar tensor $𝐴\otimes 𝐵$. It describes strings that, when prefixed by a string matching $𝐴$, will match $𝐵$.

Formally, it is defined as:

Intuitively, a parse of $𝐴⊸𝐵$ at a string $𝑣$ is a function that takes any prefix string $𝑢$ and a parse of $𝑢$ in $𝐴$, and produces a parse of the full concatenated string $𝑢·𝑣$ in $𝐵$.

For formal grammars $𝐴$ and $𝐵$, their tensor $𝐴\otimes 𝐵$ represents the concatenation of the languages they describe. A parse for $𝐴\otimes 𝐵$ at a string $𝑤$ consists of a splitting of $𝑤$ into a prefix $𝑢$ and suffix $𝑣$, along with a parse of $𝑢$ in $𝐴$ and a parse of $𝑣$ in $𝐵$.

Formally, it is defined as:

This operation is exactly the Day convolution of $𝐴$ and $𝐵$, where we view formal grammars as presheaves over the monoid of strings.

Fix a finitary algebraic theory $\mathrm{𝒯︀}$: sorts $𝑆$, a signature $𝜎$, equations, and a set $𝑉$ of generators. Write $𝑴$ for the free $\mathrm{𝒯︀}$-model on $𝑉$ and $|𝑴{|}_{𝑠}$ for its carrier at sort $𝑠$.

A $\mathrm{𝒯︀}$-type of sort $𝑠$ is a family $𝐴:|𝑴{|}_{𝑠}\to \text{𝖳𝗒𝗉𝖾}$.

For $\mathrm{𝒯︀}$-types $𝐴$ and $𝐵$ of sort $𝑠$ we have the additives, defined pointwise,

along with $\top$, $\perp$, and their indexed versions.

Each operation $𝑜:{𝑠}_0,\dots ,{𝑠}_{𝑛-1}\to 𝑠$ of $\mathrm{𝒯︀}$ gives a multiplicative, defined by Day convolution,

Each lifted operation also has closed structure: a residual in each of its arguments. Day algebras [1] give a more general convolutional definition.

When $\mathrm{𝒯︀}$ is the theory of monoids and $𝑉$ is an alphabet, $\mathrm{𝒯︀}$-types are formal grammars. Multiplication gives $\otimes$, the unit gives $𝜀$, and we recover Lambek${\begin{array}{}\end{array}}^{𝙳}$.

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