presheaf

Tag. presheaf

presheaf

Notes (22)

Predecessors simplify later predecessors-simplify-later

A predecessor of $𝑥$ is a top element of its strict downset: a strict morphism $𝜌 : 𝑝 \to 𝑥$ through which every strict morphism into $𝑥$ factors uniquely. Equivalently, $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) ≅ 𝗒 𝑝$ — the downset is representable.

The Yoneda lemma then collapses later to evaluation:

⊳ 𝑃 (𝑥) = 𝖯𝗌𝗁 𝒞︀ (𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥), 𝑃) ≅ 𝖯𝗌𝗁 𝒞︀ (𝗒 𝑝, 𝑃) ≅ 𝑃 (𝑝),

with $𝗇𝖾𝗑𝗍$ becoming restriction along $𝜌$ . The name is from the naturals: every strict map into $𝑛 + 1$ factors through $𝑛 \to 𝑛 + 1$ , so on $𝜔$ — in the topos of trees — later is just the shift

⊳ 𝑃 (0) ≅ ⊤, ⊳ 𝑃 (𝑛 + 1) ≅ 𝑃 (𝑛),

and a Löb step is a base value together with a rule producing the value at $𝑛 + 1$ from the value at $𝑛$ .

When this predecessor exists, we can give a simpler description of later, as in the topos of trees, but this may not be possible in all direct categories.

Definition. Earlier on presheaves earlier-presheaf

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, $𝗇𝖾𝗑𝗍 : 𝑃 \to ⊳ 𝑃$ corresponds to

𝗉𝗋𝖾𝗏 : ⊲ 𝑃 \to 𝑃,

Definition. Later on families later-family

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

⊳_{Fam} = 𝑈 \circ ⊳ \circ Cofree : Fam (𝒞︀) \to Fam (𝒞︀) .

Concretely, later on families evaluates to

⊳_{Fam} 𝐴 (𝑥) ≅ \prod_{𝑦 ≺ 𝑥} \prod_{𝑓 : 𝑦 \to 𝑥} 𝐴 (𝑦)

Definition. Later on presheaves later-presheaf

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 $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑦) \to 𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥)$ . 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

𝗇𝖾𝗑𝗍 : 𝑃 \to ⊳ 𝑃

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

Theorem. Löb induction on families lob-family

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

𝜑_{𝑥} : ⊳_{Fam} 𝐴 (𝑥) \to 𝐴 (𝑥) for each 𝑥,

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.

Theorem. Löb induction for presheaves on a direct category lob-presheaf

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

𝜑 : ⊳ 𝑃 \to 𝑃

has a fixed point: a global element $𝗅ö𝖻 𝜑 : ⊤ \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 $≺$ : at each $𝑥$ , the section already constructed over the past assembles into an element of $(⊳ 𝑃) (𝑥)$ , and $𝜑$ extends it to $𝑥$ .

Definition. Locally contractive endofunctors locally-contractive-functor

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

𝐹_{𝛿} : ⊳ (𝑋 \Rightarrow 𝑌) \to (𝐹 𝑋 \Rightarrow 𝐹 𝑌)

The adjoint triple between presheaves and families presheaf-family-adjoint-triple

A family over $𝒞︀$ is a set $𝐴 (𝑥)$ for each object $𝑥$ , with no action of morphisms. Families form a category $Fam (𝒞︀)$ : a morphism $𝐴 \to 𝐵$ is a function $𝐴 (𝑥) \to 𝐵 (𝑥)$ for each $𝑥$ .

Forgetting the restriction maps of a presheaf gives a functor

𝑈 : 𝖯𝗌𝗁 𝒞︀ \to Fam (𝒞︀) .

It has both a left and a right adjoint,

Free ⊣ 𝑈 ⊣ Cofree .

The two adjoints demonstrate different means of forcing a family to be functorial. The right adjoint universally quantifies over morphisms in,

Cofree (𝐴) (𝑥) = \prod_{𝑦} 𝒞︀ (𝑦, 𝑥) \to 𝐴 (𝑦),

with restriction along $𝑓$ given by precomposition. The left adjoint instead existentially quantifiers over morphisms out:

Free (𝐴) (𝑥) = \sum_{𝑦} 𝒞︀ (𝑥, 𝑦) \times 𝐴 (𝑦),

with restriction acting on the first component. (For $Free$ we ask that $𝒞︀$ have a set of objects, so that this sum is a set and thus $Free$ defines a presheaf.)

Theorem. Presheaves are monadic and comonadic over families presheaves-monadic-comonadic-over-families

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

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

𝖯𝗌𝗁 𝒞︀ ≃ EM (𝑇) 𝖯𝗌𝗁 𝒞︀ ≃ coEM (𝑊) .

So presheaves are both monadic and comonadic over families.

Reading the algebra structure concretely: a $𝑇$ -algebra on a family $𝐴$ is a map $\sum_{𝑦} 𝒞︀ (𝑥, 𝑦) \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_{𝑦} 𝒞︀ (𝑦, 𝑥) \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.

Definition. Proper and maximal sieves proper-maximal-sieve

The representable $𝗒 𝑥$ 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.

Definition. Sieves sieve

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

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

𝑆 ∋ 𝑓 \Rightarrow 𝑆 ∋ 𝑔 ⋆ 𝑓 for every 𝑔 : 𝑧 \to 𝑦 .

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

Theorem. Maximality of the strict downset among proper sieves strict-downset-maximal

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:

𝑆 \subseteq 𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) .

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

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

Definition. The strict downset sieve of a direct category strict-downset-sieve

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

𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) (𝑦) = {𝑓 : 𝑦 \to 𝑥 ∣ 𝑦 ≺ 𝑥},

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

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

Definition. Element of a Presheaf element-of-presheaf

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

Definition. Universal Element of a Presheaf universal-element

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.

What is a universal property, really? universal-property

Universal properties are a convenient method for defining an object in a category up to isomorphism. Rather than giving a concrete, bottom-up construction of an object, we can instead uniquely specify its behavior.

Consider the example of products in a category $𝐶$ . We say that the product of $𝑐$ and $𝑑$ is any object $𝑝$ of $𝐶$ such that the following diagram commutes.

We say that $𝑝$ satisfies the universal property of the product of $𝑐$ and $𝑑$ .

Surely this matches our set-based intuition of what a product should behave like. Similarly, we can sketch out constructions of other universal properties like initial objects, terminal objects, exponentials, etc. However, what is precisely meant by the term universal property?

The notion of a universal property is made precise by the notion of a universal element of a presheaf. That is, an object satisfies a universal property if we can build a universal element of the appropriate presheaf at that object.

Let’s look at the universal element characterization of the products example. Note that a map into a product is determined by a map into each component. To map into $𝑐 \times 𝑑$ , we need both a map into $𝑐$ and a map into $𝑑$ , as in the above diagram. That is, to build a map $𝑏 \to 𝑐 \times 𝑑$ , we must simultaneously provide elements of $よ 𝑐$ and $よ 𝑑$ at $𝑏$ .

Using the product of presheaves, this means we are providing a single element of the presheaf $(よ 𝑐) \times (よ 𝑑)$ . Quite nicely, the universal element of this presheaf provides the object of $𝐶$ that is the product of $𝑐$ and $𝑑$ . The universal element, provided that it exists, contains the following data:

An object $𝑝$
An element $𝑥 \in (よ 𝑐 \times よ 𝑑) 𝑝$
A proof that the map sending $𝑓 : 𝑏 \to 𝑝$ to a pair of maps $𝑓_{1} : 𝑏 \to 𝑐$ , $𝑓_{2} : 𝑏 \to 𝑑$ is an equivalence. Therefore, any element of $よ 𝑐 \times よ 𝑑$ factors through $𝑥$

Recall that the product of presheaves is computed pointwise in the category of sets, so if we expand the type of the element $𝑥$ above we find that $𝑥$ is a pair of maps $𝑝 \to 𝑐$ and $𝑝 \to 𝑑$ .

(よ 𝑐 \times よ 𝑑) 𝑝 ≅ (よ 𝑐 𝑝) \times (よ 𝑑 𝑝)

The first part of this pair is precisely $𝜋_{1}$ . Correspondingly, the second part of this pair is $𝜋_{2}$ . Finally, the universality of the element $𝑥$ (i.e. the proof that any other element factors through $𝑥$ ) captures our commutative diagram from above.

This is a very rough sketch of what a universal property is, and has elided for now an important application of the Yoneda lemma. In any case, all a universal property is really saying is that a particular presheaf is representable; and, rather elegantly, a universal element of a presheaf is convenient packaging of that representability proof.

In summary, universal properties are not as ad-hoc as they may initially seem, and the language of presheaves provides a reusable and precise definition that can be instantiated to describe a very large class of properties.

Definition. Constant Presheaf constant-presheaf

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

Δ (𝑋) 𝑐 ≔ 𝑋

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

Finite Cardinal Arithmetic in a Topos finite-cardinal-arithmetic-topos

In a topos with a natural numbers object $(𝑁, 𝑧, 𝑠)$ , you can define finite cardinals as objects that arise as the pullback along a morphism $𝑝 : ⊤ \to 𝑁$ of the generic finite cardinal. Write $[𝑝]$ for the cardinal corresponding to $𝑝$ .

The above characterization is a little obtuse and does warrant some more explanation. One way to make it more concrete is that $[𝑧] = ⊥$ and $[𝑠 \circ 𝑛] = ⊤ \oplus [𝑛]$ , and that finite cardinals warrant a nice induction principle. If $𝑃$ is a property expressible in the internal language such that $⊥$ satisfies $𝑃$ , and that whenever $𝐴$ satisfies $𝑃$ then $⊤ \oplus 𝐴$ satisfies $𝑃$ ; then every finite cardinal satisfies $𝑃$ . That is, $𝑃$ forms a $(𝑧, 𝑠)$ -closed subobject of $𝑁$ and thus $𝑃$ is all of $𝑁$ .

My working mental model is in a presheaf topos, where the natural numbers object can be defined explicitly as $Δ (ℕ)$ .

Definition 0.1. Constant Presheaf constant-presheaf

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

Δ (𝑋) 𝑐 ≔ 𝑋

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

The finite cardinals with respect to $Δ (ℕ)$ can be characterized then as,

[0] ≔ ⊥

[𝗌𝗎𝖼 (𝑛)] ≔ ⊤ \oplus [𝑛]

These obey nice algebraic properties.

[𝑛 𝑚] ≅ [𝑛] \times [𝑚]

[𝑛 + 𝑚] ≅ [𝑛] \oplus [𝑚]

[𝑛^{𝑚}] ≅ [𝑚] \to [𝑛]

Definition. Category of Elements category-of-elements

Let $𝑃$ be a presheaf on a category $𝒞︀$ . The category of elements of $𝑃$ is the displayed category over $𝒞︀$ 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 $𝒞︀$ 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 𝑃$ .

Theorem. Day Convolution is Closed day-closed-structure

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

(𝐴 ⊸ 𝐵) 𝑐 = \int_{𝑢} 𝐴 𝑢 ⊸_{𝒱︀} 𝐵 (𝑢 \otimes_{𝒞︀} 𝑐) .

Then, for Day convolution $\otimes_{Day}$ ,

𝐴 \otimes_{Day} - ⊣ 𝐴 ⊸_{Day} - .

Proof. Proof that Day Convolution is Closed day-closed-structure-proof

For $𝑋, 𝐵 : {𝒞︀}^{op} \to 𝒱︀$ , the enriched hom in $[{𝒞︀}^{op}, 𝒱︀]$ is given by the end:

\begin{aligned} \int_{𝑐} ((𝐴 \otimes_{Day} 𝑋) 𝑐 ⊸_{𝒱︀} 𝐵 𝑐) & ≅ \int_{𝑐} ((\int^{𝑢, 𝑣} 𝒞︀ (𝑐, 𝑢 \otimes_{𝒞︀} 𝑣) \otimes_{𝒱︀} 𝐴 𝑢 \otimes_{𝒱︀} 𝑋 𝑣) ⊸_{𝒱︀} 𝐵 𝑐) \\ ≅ \int_{𝑐} \int_{𝑢, 𝑣} ((𝒞︀ (𝑐, 𝑢 \otimes_{𝒞︀} 𝑣) \otimes_{𝒱︀} 𝐴 𝑢 \otimes_{𝒱︀} 𝑋 𝑣) ⊸_{𝒱︀} 𝐵 𝑐) \\ ≅ \int_{𝑢, 𝑣} ((𝐴 𝑢 \otimes_{𝒱︀} 𝑋 𝑣) ⊸_{𝒱︀} \int_{𝑐} (𝒞︀ (𝑐, 𝑢 \otimes_{𝒞︀} 𝑣) ⊸_{𝒱︀} 𝐵 𝑐)) \\ ≅ \int_{𝑢, 𝑣} ((𝐴 𝑢 \otimes_{𝒱︀} 𝑋 𝑣) ⊸_{𝒱︀} 𝐵 (𝑢 \otimes_{𝒞︀} 𝑣)) \\ ≅ \int_{𝑣} (𝑋 𝑣 ⊸_{𝒱︀} \int_{𝑢} (𝐴 𝑢 ⊸_{𝒱︀} 𝐵 (𝑢 \otimes_{𝒞︀} 𝑣))) \\ ≅ \int_{𝑣} (𝑋 𝑣 ⊸_{𝒱︀} (𝐴 ⊸ 𝐵) 𝑣) . \end{aligned}

∎

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

Definition. Day Convolution day-convolution

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

(𝐴 \otimes_{Day} 𝐵) 𝑐 = \int^{𝑢, 𝑣} 𝒞︀ (𝑐, 𝑢 \otimes_{𝒞︀} 𝑣) \otimes_{𝒱︀} 𝐴 𝑢 \otimes_{𝒱︀} 𝐵 𝑣,

with unit the representable $𝒞︀ (-, 𝐼)$ .

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

Under the enriched Yoneda embedding the convolution of representables is representable, $𝒞︀ (-, 𝑥) \otimes_{Day} 𝒞︀ (-, 𝑦) ≅ 𝒞︀ (-, 𝑥 \otimes_{𝒞︀} 𝑦)$ , so Day convolution is the cocontinuous extension of the tensor of $𝒞︀$ .

As a Kan Extension

Equivalently, $𝐴 \otimes_{Day} 𝐵$ is the left Kan extension of $(𝑢, 𝑣) \mapsto 𝐴 𝑢 \otimes_{𝒱︀} 𝐵 𝑣$ along $\otimes_{𝒞︀}^{op} : {𝒞︀}^{op} \times {𝒞︀}^{op} \to {𝒞︀}^{op}$ .

In $𝐒𝐞𝐭$

When $𝒱︀ = 𝐒𝐞𝐭$ , we recover the ordinary Day convolution of presheaves $𝐴, 𝐵 : {𝒞︀}^{op} \to 𝐒𝐞𝐭$ , where the formula simplifies to:

(𝐴 \otimes_{Day} 𝐵) 𝑐 = \int^{𝑢, 𝑣} 𝒞︀ [𝑐, 𝑢 \otimes_{𝒞︀} 𝑣] \times 𝐴 𝑢 \times 𝐵 𝑣 .

Theorem. Next on Grammars Is Presheaf Structure grammar-next-presheaf

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

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

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

Löb does not need $𝗇𝖾𝗑𝗍$ on $𝐴$ . The fixed-point equation only restricts a global parse $⊤ ⊢ 𝐴$ , 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 $𝑐 ++ 𝑡$ is represented by $𝑡$ , because every proper suffix of $𝑐 ++ 𝑡$ is a suffix of $𝑡$ . So predecessors simplify later to $(▷ 𝑃) (𝑐 ++ 𝑡) ≅ 𝑃 𝑡$ . On grammars there is no such simplification, since the factors at different suffixes are unrelated.